GADT type inference with higher level types

Question

I have code that compiles:

{-# LANGUAGE ScopedTypeVariables, KindSignatures, GADTs, FlexibleContexts #-} module Foo where data Foo :: (* -> *) where Foo :: cm zp' -> Foo (cm zp) f :: forall cm zp d . Foo (cm zp) -> d f y@ (Foo (x :: cma)) = gxy g :: cma -> Foo (cmb) -> d g = error "" 

The key point in my real code is to convince the GHC that if y is of type Foo (cm zp) and x is of type c' m' zp' , then c' ~ c and m' ~ m . The above code achieves this because I can call g .

I want to change this code in two orthogonal ways, but I cannot figure out how to get GHC to compile the code with any change.

First change: Add -XPolyKinds . GHC 7.8.3 complains:

 Foo.hs:10:11: Could not deduce ((~) (k2 -> k3 -> *) c1 c) from the context ((~) * (cm zp) (c1 m1 zp1)) bound by a pattern with constructor Foo :: forall (k :: BOX) (k :: BOX) (c :: k -> k -> *) (m :: k) (zp' :: k) (zp :: k). cm zp' -> Foo (cm zp), in an equation for 'f' at Foo.hs:10:6-21 'c1' is a rigid type variable bound by a pattern with constructor Foo :: forall (k :: BOX) (k :: BOX) (c :: k -> k -> *) (m :: k) (zp' :: k) (zp :: k). cm zp' -> Foo (cm zp), in an equation for 'f' at Foo.hs:10:6 'c' is a rigid type variable bound by the type signature for f :: Foo (cm zp) -> d at Foo.hs:9:13 Expected type: c1 m1 zp' Actual type: cma Relevant bindings include y :: Foo (cm zp) (bound at Foo.hs:10:3) f :: Foo (cm zp) -> d (bound at Foo.hs:10:1) In the pattern: x :: cma In the pattern: Foo (x :: cma) In an equation for 'f': f y@ (Foo (x :: cma)) = gxy Foo.hs:10:11: Could not deduce ((~) k2 m1 m) from the context ((~) * (cm zp) (c1 m1 zp1)) ... 

Second change: Forget about -XPolyKinds . Instead, I want to use -XDataKinds to create a new type and restriction of type m :

 {-# LANGUAGE ScopedTypeVariables, KindSignatures, GADTs, FlexibleContexts, DataKinds #-} module Foo where data Bar data Foo :: (* -> *) where Foo :: c (m :: Bar) zp' -> Foo (cm zp) f :: forall cm zp d . Foo (cm zp) -> d f y@ (Foo (x :: cma)) = gxy g :: cma -> Foo (cmb) -> d g = error "" 

I get similar errors ( can't deduce (c1 ~ c) , can't deduce (m1 ~ m) ). DataKinds seems relevant here: if I restrict m to have a Constraint look instead of a kind Bar , the code compiles fine.

---

I gave two examples of how to break the source code, both of which use higher-grade types. I tried using case arguments instead of template protection, I tried giving node type instead of x , my usual tricks here do not work.

I don’t understand where the type for x / ends, how it looks, I just need to convince GHC that if y is of type Foo (cm zp) , then x is of type cm zp' for some unrelated type zp' .

Answer 1

I greatly simplified the original question to the next one, which compiles without {-# LANGUAGE PolyKinds #-} , but does not compile with PolyKinds .

 {-# LANGUAGE ScopedTypeVariables, KindSignatures, GADTs #-} {-# LANGUAGE PolyKinds #-} data Pair1 :: (* -> *) where Pair1 :: Pair1 (ca, cb) data D pa where D :: p (a, b) -> D pa -> D pb f :: forall c z. D Pair1 (cz) -> D Pair1 (cz) f y@ (D Pair1 x) | (_ :: D Pair1 (cz)) <- y, (_ :: D Pair1 (c z')) <- x = y 

PolyKinds Error PolyKinds with PolyKinds

 Could not deduce (c1 ~ c) from the context ((a, cz) ~ (c1 a1, c1 b)) 

This error strongly indicates that I already suspected that the answer depends on whether the polyciform application is injective . If the use of the polycid type was injective, we could draw the conclusion c1 ~ c as follows.

 (a, cz) ~ (c1 a1, c1 b) (a,) (cz) ~ (c1 a1,) (c1 b) {- switch to prefix notation -} cz ~ c1 b {- fa ~ gb implies a ~ b -} c ~ c1 {- fa ~ gb implies f ~ g -} c1 ~ c {- ~ is reflexive -} 

An application like Polykinded is injective , but ghc doesn't know that. In order for ghc to deduce that the type application is injective, we need to provide good signatures so that the compiler knows that the views are equivalent.

I did not find enough annotations for your original, too simplified version of the problem. When simplifying juggling types of problems, reducing the type of Proxy in essence is sometimes excessive, as it leaves less room for attaching type signatures. You have found places to attach the view signature to a more significant problem.

Answer 2

The problem can be solved by adding view signatures.

For example, when using -XPolyKinds following code compiles:

 {-# LANGUAGE ScopedTypeVariables, KindSignatures, GADTs, FlexibleContexts, PolyKinds #-} module Foo where data Foo :: (* -> *) where Foo :: (c :: k -> * -> *) m zp' -> Foo (cm zp) f :: forall (c :: k -> * -> *) m zp d . Foo (cm zp) -> d f y@ (Foo x) = gxy g :: cma -> Foo (cmb) -> d g = error "" 

For the -XDataKinds version -XDataKinds I also need a signature like g :

 {-# LANGUAGE ScopedTypeVariables, KindSignatures, GADTs, FlexibleContexts, DataKinds #-} module Foo where data Bar data Foo :: (* -> *) where Foo :: (c :: Bar -> * -> *) m zp' -> Foo (cm zp) f :: forall (c :: Bar -> * -> *) m zp d . Foo (cm zp) -> d f y@ (Foo x) = gxy g :: forall (c :: Bar -> * -> *) mabd . cma -> Foo (cmb) -> d g = error "" 

Not sure why I need more sigs for DataKinds , and it is a little annoying to copy them everywhere, but it does its job.