Strange errors when using type families as parameters
I seem to have found a dark corner of GHC. In the process of finding a minimal example, I found a few different ways to trigger a bug. I'm assuming they are all related.
Example 1
I started off with a GADT parameterized by a type list:
{-# LANGUAGE TypeFamilies, GADTs, DataKinds, TypeOperators #-}
module Foo where
type TList = '[Float, Double]
type family PrevElt (xs :: [*]) (a :: *) :: * where
PrevElt (b ': a ': xs) a = b
PrevElt (b ': c ': xs) a = PrevElt (c ': xs) a
data FooList :: ([*] -> * -> *) where
Bar :: FooList prevrp ((PrevElt prevrp rp) -> rp)
test1 :: FooList TList ((PrevElt TList rp) -> rp)
test1 = Bar
which compiles as expected.
If I make a syntactic change and parameterize the GADT with the type family rather than the type list:
{-# LANGUAGE TypeFamilies, GADTs, DataKinds, TypeOperators #-}
module Foo where
type TList = '[Float, Double]
type family PrevElt (xs :: [*]) (a :: *) :: * where
PrevElt (b ': a ': xs) a = b
PrevElt (b ': c ': xs) a = PrevElt (c ': xs) a
data FooTF :: ((* -> *) -> * -> *) where
Bar :: FooTF prevrp ((prevrp rp) -> rp)
test2 :: FooTF (PrevElt TList) ((PrevElt TList rp) -> rp)
test2 = Bar
I get a non-sensical error:
Foo.hs:15:9:
Couldn't match type `PrevElt TList rp' with `PrevElt TList rp'
NB: `PrevElt' is a type function, and may not be injective
Expected type: FooTF (PrevElt TList) (PrevElt TList rp -> rp)
Actual type: FooTF (PrevElt TList) (PrevElt TList rp -> rp)
Relevant bindings include
test2 :: FooTF (PrevElt TList) (PrevElt TList rp -> rp)
(bound at testsuite\Foo.hs:15:1)
In the expression: Bar
In an equation for `test2': test2 = Bar
As far as I know, this should compile.
Example 2
Another simple example uses syntactic, along with the type-family-parameterized GADT:
{-# LANGUAGE TypeFamilies, GADTs, DataKinds, TypeOperators #-}
module Foo where
import Data.Syntactic
type family PrevElt (xs :: [*]) (a :: *) :: * where
PrevElt (b ': a ': xs) a = b
PrevElt (b ': c ': xs) a = PrevElt (c ': xs) a
data FooTF :: ((* -> *) -> * -> *) where
Const :: FooTF prevrp (Full rp)
Bar :: FooTF prevrp ((prevrp rp) :-> Full rp)
type T1 = Double
type T2 = Float
type Dom = FooTF (PrevElt '[T1, T2])
leaf = inj (Const :: Dom (Full T1)) :: ASTF Dom T1
t1 = inj (Bar :: Dom (T1 :-> Full T2)) :$ leaf :: ASTF Dom T2
By only changing the types T1
and T2
:
{-# LANGUAGE TypeFamilies, GADTs, DataKinds, TypeOperators #-}
module Foo where
import Data.Syntactic
type family PrevElt (xs :: [*]) (a :: *) :: * where
PrevElt (b ': a ': xs) a = b
PrevElt (b ': c ': xs) a = PrevElt (c ': xs) a
data FooTF :: ((* -> *) -> * -> *) where
Const :: FooTF prevrp (Full rp)
Bar :: FooTF prevrp ((prevrp rp) :-> Full rp)
data T a
type T1 = T Double
type T2 = T Float
type Dom = FooTF (PrevElt '[T1, T2])
leaf = inj (Const :: Dom (Full T1)) :: ASTF Dom T1
t1 = inj (Bar :: Dom (T1 :-> Full T2)) :$ leaf :: ASTF Dom T2
GHC complains:
Foo.hs:21:11:
Couldn't match type ‘Double’ with ‘T Float’
Expected type: Dom (T1 :-> Full T2)
Actual type: FooTF T (T Double :-> Full Double)
In the first argument of ‘inj’, namely
‘(Bar :: Dom (T1 :-> Full T2))’
In the first argument of ‘(:$)’, namely
‘inj (Bar :: Dom (T1 :-> Full T2))’
Failed, modules loaded: none.
Example 3
I've also attached a larger example (also using syntactic) that has [more, different] errors, which I believe to be related to this problem. Errors for the attached file are:
Foo.hs:32:6:
Couldn't match type `NextElt TList (PrevElt ((':) * (T' Float) ('[] *)) Double)'
with `Double'
Expected type: Double
Actual type: NextElt TList (PrevElt TList Double)
In the first argument of `(:$)', namely `inj' Bar'
In the expression: inj' Bar :$ leaf
In an equation for `t1': t1 = inj' Bar :$ leaf
Foo.hs:32:11:
Couldn't match type `PrevElt TList' with T'
Expected type: Dom (Foo (T' Double) T1 :-> Full (Foo Double T1))
Actual type: FooTF
T' (Foo (T' Double) T1 :-> Full (Foo Double T1))
In the first argument of inj', namely `Bar'
In the first argument of `(:$)', namely `inj' Bar'
In the first error, the Actual type: NextElt TList (PrevElt TList Double)
is strange because Double
only occurs as a parameter to T'
, and never as a naked type that could be applied to type family.
In the second error, GHC seems to be confusing two types of kind (* -> *)
: T'
and PrevElt TList
.
Changing the GADT from type-family-indexed to type-list-index (like in the first example) makes the attached code compile. I minimized the attached example as much as possible: any changes I made to simplify the code resulted in different errors, which may also be helpful for finding this bug.