{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, GADTs, TypeOperators,
ScopedTypeVariables, TemplateHaskell, FlexibleInstances,
ConstraintKinds, UndecidableInstances, TemplateHaskell #-}
module A where
data TyArr (a :: *) (b :: *) :: *
type family (a :: TyArr k1 k2 -> *) @@ (b :: k1) :: k2
data TyPi (a :: *) (b :: TyArr a * -> *) :: *
type family (a :: TyPi k1 k2 -> *) @@@ (b :: k1) :: k2 @@ b
data A (x :: TyArr Bool *) :: *
type instance A @@ 'False = ()
type instance A @@ 'True = ((), ())
data B (x :: TyPi Bool A) :: *
type instance B @@@ 'False = '()
type instance B @@@ 'True = '( '(), '())
produces
A.hs:18:30:
Expected kind ‘A @@ 'False’, but ‘'()’ has kind ‘()’
In the type ‘()’
In the type instance declaration for ‘@@@’
A.hs:18:30:
Expected kind ‘A @@ 'False’, but ‘'()’ has kind ‘()’
In the type ‘()’
In the type instance declaration for ‘@@@’
A.hs:19:30:
Expected kind ‘A @@ 'True’, but ‘'('(), '())’ has kind ‘((), ())’
In the type ‘'((), ())’
In the type instance declaration for ‘@@@’
A.hs:19:30:
Expected kind ‘A @@ 'True’, but ‘'('(), '())’ has kind ‘((), ())’
In the type ‘'((), ())’
In the type instance declaration for ‘@@@’
This is just lack of dependency analysis on instances. Making the Issue so we get a regression test.
From @RafaelBocquet, extracted from #31:
produces
This is just lack of dependency analysis on instances. Making the Issue so we get a regression test.