Search code examples
haskelltypeerror

haskell strange type error when using point-free notation with (.) operator

Can someone please explain to me why this code doesn't work:

import GHC.Exts (build)
data List a = Nil | Cons a (List a)

toLambdaList :: List t0 -> (t0 -> t1 -> t1) -> t1 -> t1
toLambdaList Nil cons nil = nil
toLambdaList (x `Cons` xs) cons nil = x `cons` (toLambdaList xs cons nil)
fromList :: List a -> [a]
fromList = build . toLambdaList

the error I'm getting is this:

Couldn't match type: forall b. (a -> b -> b) -> b -> b
               with: (t1 -> t20 -> t20) -> t20 -> t20

(GHCi version 9.0.2)

Suprisingly, if I just replace build . toLambdaList with \a -> build $ toLambdaList a, the new code suddenly works:

import GHC.Exts (build)
data List a = Nil | Cons a (List a)

toLambdaList :: List t0 -> (t0 -> t1 -> t1) -> t1 -> t1
toLambdaList Nil cons nil = nil
toLambdaList (x `Cons` xs) cons nil = x `cons` (toLambdaList xs cons nil)
fromList :: List a -> [a]
fromList a = build $ toLambdaList a

I've tried deleting type declarations, but this doesn't help.

Solution

  • The reason why this doesn't work (since GHC 9) is that forall is treated more literally now in types. In your case the types

    In your case the compiler complains that it cannot match these types:

       Expected: ((a -> t1 -> t1) -> t1 -> t1) -> [a]
     Actual: (forall b. (a -> b -> b) -> b -> b) -> [a]

    They do look different, but you may expect that GHC would just instantiate that forall b in the actual type to t1. Then the types would match. That is what GHC used to do before version 9 and can now be re-enabled with a new extension called DeepSubsumption in GHC 9.2 and later.

    GHC does still instantiate forall'd variables in some cases, but not when it is below the left side of a function arrow such as in your case.

    The main reasons for making this change were:

    • It simplifies the type checker.
    • It makes it possible to support impredicative types properly.
    • These instantiations would silently affect runtime behavior.

    For more details see the Simplify Subsumption proposal.

    One way you can solve this is by using ImpredicativeTypes (which can be a replacement for deep subsumption in some cases) and changing the type of toLambdaList a little:

    {-# LANGUAGE ImpredicativeTypes #-}

import GHC.Exts (build)
data List a = Nil | Cons a (List a)

toLambdaList :: List t0 -> forall t1. (t0 -> t1 -> t1) -> t1 -> t1
toLambdaList Nil cons nil = nil
toLambdaList (x `Cons` xs) cons nil = x `cons` (toLambdaList xs cons nil)
fromList :: List a -> [a]
fromList = build . toLambdaList

    To understand why this works we need to look at the type of (.):

    (.) :: forall a b c. (b -> c) -> (a -> b) -> a -> c

    Using ImpredicativeTypes we can instantiate b to be forall t1. (t0 -> t1 -> t1) -> t1 -> t1. And a and b are instantiated as usual to List a and [a] respectively. The specialised type of (.) then becomes:

    (.) :: forall a t0.
  ((forall t1. (t0 -> t1 -> t1) -> t1 -> t1) -> [a]) ->
  (List a -> forall t1. (t0 -> t1 -> t1) -> t1 -> t1) ->
  List a -> [a]

    Now the type of the first argument matches the type of build and the type of the second argument matches the type of toLambdaList.