Open goldfirere opened 9 years ago
Here is (maybe) another instance of the same issue :
module A where
import Prelude ()
import qualified Prelude as P
data TyFun' (a :: *) (b :: *) :: *
type TyFun (a :: *) (b :: *) = TyFun' a b -> *
type family (a :: TyFun k1 k2) @@ (b :: k1) :: k2
data TyPi' (a :: *) (b :: TyFun a *) :: *
type TyPi (a :: *) (b :: TyFun a *) = TyPi' a b -> *
type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b
data CY (a :: *) (b :: a) (c :: TyFun' a *)
type instance (@@) (CY a b) c = *
data CX (a :: *) (b :: TyFun' a *)
type instance (@@) (CX a) b = TyPi a (CY a b)
$(P.return [])
data DG (a :: *) (b :: TyPi a (CX a)) (c :: a) (d :: a) (e :: TyFun' (b @@@ d @@@ c) *)
$(P.return [])
type instance (@@) (DG a b c d) e = ()
OUT.hs:29:15:
Illegal type synonym family application in instance:
(b @@@ d) @@@ c
In the type instance declaration for ‘@@’
This prevents me from extracting some types when arguments have function types.
I do believe your code is an instance of this issue. Generally, using any type family in the declared kind of another type family will tickle this. I'm afraid this one isn't so quick to fix, having already looked into it and been blocked myself. I can prioritize this after July 10 (the POPL deadline), but I don't think I can look into it before then, as the POPL paper still needs lots of work.
When I say
I get
Solution: invent a new flavor of metavariable that stubbornly refuses to unify with a type family. Also, make sure to abstract out coercions in type family patterns.