Haskell unexpected `forall` in typechecking failure-CodePudding

I am working on a mathematics project with a persistent need of extracting a canonical "basis" out of a type, so I defined the following type class.

class Basis a where
    getBasis :: Int -> [a]

And I want to use this basis in a separate function:

foo :: (Basis a) => Int -> (a -> b) -> IO ()
foo n f = do
    let theBasis = getBasis n
    undefined
    -- Do some stuff with the basis using the function f.
    -- theBasis should have type [a].

However this fails to type check, yielding an error of the form Could not deduce (Basis a0) arising from the use of 'getBasis' from the context: Basis a.

I tried to help the typechecker by explicitly writing the expected type:

foo n f = do
    let theBasis = (getBasis n) :: [a]
    undefined

But the error persists, and moving the type annotation to different terms in that line does not fix the error.

How can I tell the typechecker that I want the type of getBasis n to be the same a appearing in the signature of foo?

CodePudding user response：

The easiest way to do this in this case would be to just use the basis for something, because then the typechecker can infer which a you meant:

Silly example:

foo :: Basis a => Int -> (a -> b) -> IO ()
foo n f = do
    let theBasis = getBasis n
        _        = map f theBasis
    undefined

Otherwise you can also use type annotations (requires the ScopedTypeVariables extension, without that the a inside the function body won't be the a from the signature):

foo :: forall a b. Basis a => Int -> (a -> b) -> IO ()
foo n f = do
    let theBasis = getBasis n :: [a]
    undefined

With ScopedTypeVariables TypeApplications you can also explicitly pass the type parameter a along to getBasis:

foo :: forall a b. Basis a => Int -> (a -> b) -> IO ()
foo n f = do
    let theBasis = getBasis @a n
    undefined

CodePudding user response：

The original error happens likely because you don't have anything further in the code which would indicate the type of theBasis to the compiler. For example, if you're only using it in an expression like show theBasis, then all the compiler knows is that the type should have a Show instance, but it still doesn't know what the type is.

Your attempt to fix, however, is more interesting. It sheds light on the underlying problem. Even if you explicitly specify that the type should be [a], the compiler is still confused. Why is that? You said it's [a], what else could the compiler want?

And the answer is that the a in (Basis a) and the a in :: [a] are not the same a!

In Haskell, by default, the scope of type variables is limited to only the type signature in which they're used. So in the type signature of foo it's one a, local to that type signature. And then in type signature of (getBasis n) it's a totally different a, local to that type signature.

But there is a way to tell the compiler that it should be the same a. That way is forall:

foo :: forall a b. (Basis a) => Int -> (a -> b) -> IO ()
foo n f = do
    let theBasis = (getBasis n) :: [a]
    undefined

When used explicitly, forall creates a wider scope for type variables listed in it. For function type signatures, the scope is the whole body of the function. Thus, the a in :: [a] ends up being the same a as in foo's signature.

(note that you need either the ScopedTypeVariables extension for this to work)

CodePudding user response：

Use ScopedTypeVariables. This extension allows to use the type variable in the type signature within the function body. Notice, In some context I a can be deduce from f, so you get rid of the error

{-# LANGUAGE ScopedTypeVariables #-}

class Basis a where
    getBasis :: Int -> [a]


foo :: forall a b. (Basis a) => Int -> (a -> b) -> IO ()
foo n f = do
    let theBasis = getBasis n :: [a]
    undefined
    -- Do some stuff with the basis using the function f.
    -- theBasis should have type [a].