Type inference is weaker for GADT than analogous Data Family
I'm marking this as a Feature request rather than a bug (though it was unexpected behavior for me!)
In my code base i had the following types
data Prod = Pair Prod Prod | Unit
data VProd (vect :: * -> * ) (prd:: Prod ) val where
VLeaf :: !(v a) -> VProd v Unit a
VPair :: !(VProd v pra a) -> !(VProd v prb b ) ->VProd v (Pair pra prb) (a,b)
data MVProd (vect :: * -> * -> * ) (prd:: Prod ) (st :: * ) val where
MVLeaf :: !(mv st a) -> MVProd mv Unit st a
MVPair :: !(MVProd mv pra st a) -> !(MVProd mv prb st b ) -> MVProd mv (Pair pra prb) st (a,b)
which are meant as a way of modeling vectors of tuples as tuples (err trees) of vectors
however, sometimes type inference would fail in explosive ways like
*Numerical.Data.Vector.Pair Data.Vector VG> (VPair (VLeaf (va :: Vector Int)) (VLeaf (vb:: Vector Int))) <- return $ VG.fromList [(1::Int,2::Int),(3,5)] :: (VProd Vector (Pair Unit Unit) (Int,Int))
<interactive>:24:16:
Could not deduce (a ~ Int)
from the context (t1 ~ 'Pair pra prb, t2 ~ (a, b))
bound by a pattern with constructor
VPair :: forall (v :: * -> *) (pra :: Prod) a (prb :: Prod) b.
VProd v pra a -> VProd v prb b -> VProd v ('Pair pra prb) (a, b),
in a pattern binding in
interactive GHCi command
at <interactive>:24:2-59
or from (pra ~ 'Unit)
bound by a pattern with constructor
VLeaf :: forall (v :: * -> *) a. v a -> VProd v 'Unit a,
in a pattern binding in
interactive GHCi command
at <interactive>:24:9-32
‘a’ is a rigid type variable bound by
a pattern with constructor
VPair :: forall (v :: * -> *) (pra :: Prod) a (prb :: Prod) b.
VProd v pra a -> VProd v prb b -> VProd v ('Pair pra prb) (a, b),
in a pattern binding in
interactive GHCi command
at <interactive>:24:2
Expected type: t0 a
Actual type: Vector Int
In the pattern: va :: Vector Int
In the pattern: VLeaf (va :: Vector Int)
In the pattern:
VPair (VLeaf (va :: Vector Int)) (VLeaf (vb :: Vector Int))
<interactive>:24:43:
Could not deduce (b ~ Int)
from the context (t1 ~ 'Pair pra prb, t2 ~ (a, b))
bound by a pattern with constructor
VPair :: forall (v :: * -> *) (pra :: Prod) a (prb :: Prod) b.
VProd v pra a -> VProd v prb b -> VProd v ('Pair pra prb) (a, b),
in a pattern binding in
interactive GHCi command
at <interactive>:24:2-59
or from (pra ~ 'Unit)
bound by a pattern with constructor
VLeaf :: forall (v :: * -> *) a. v a -> VProd v 'Unit a,
in a pattern binding in
interactive GHCi command
at <interactive>:24:9-32
or from (prb ~ 'Unit)
bound by a pattern with constructor
VLeaf :: forall (v :: * -> *) a. v a -> VProd v 'Unit a,
in a pattern binding in
interactive GHCi command
at <interactive>:24:36-58
‘b’ is a rigid type variable bound by
a pattern with constructor
VPair :: forall (v :: * -> *) (pra :: Prod) a (prb :: Prod) b.
VProd v pra a -> VProd v prb b -> VProd v ('Pair pra prb) (a, b),
in a pattern binding in
interactive GHCi command
at <interactive>:24:2
Expected type: t0 b
Actual type: Vector Int
In the pattern: vb :: Vector Int
In the pattern: VLeaf (vb :: Vector Int)
In the pattern:
VPair (VLeaf (va :: Vector Int)) (VLeaf (vb :: Vector Int))
<interactive>:24:65:
Couldn't match type ‘(Int, Int)’ with ‘Int’
Expected type: VProd Vector ('Pair 'Unit 'Unit) (Int, Int)
Actual type: VProd Vector ('Pair 'Unit 'Unit) (Int, (Int, Int))
In the first argument of ‘GHC.GHCi.ghciStepIO ::
IO a_a5BR -> IO a_a5BR’, namely
‘return $ VG.fromList [(1 :: Int, 2 :: Int), (3, 5)] ::
VProd Vector (Pair Unit Unit) (Int, Int)’
In a stmt of an interactive GHCi command:
(VPair (VLeaf (va :: Vector Int))
(VLeaf (vb :: Vector Int))) <- GHC.GHCi.ghciStepIO ::
IO a_a5BR -> IO a_a5BR
(return $ VG.fromList [(1 :: Int, 2 :: Int), (3, 5)] ::
VProd Vector (Pair Unit Unit) (Int, Int))
<interactive>:24:65:
Couldn't match expected type ‘IO (VProd t0 t1 t2)’
with actual type ‘VProd Vector ('Pair 'Unit 'Unit) (Int, Int)’
In the first argument of ‘GHC.GHCi.ghciStepIO ::
IO a_a5BR -> IO a_a5BR’, namely
‘return $ VG.fromList [(1 :: Int, 2 :: Int), (3, 5)] ::
VProd Vector (Pair Unit Unit) (Int, Int)’
In a stmt of an interactive GHCi command:
(VPair (VLeaf (va :: Vector Int))
(VLeaf (vb :: Vector Int))) <- GHC.GHCi.ghciStepIO ::
IO a_a5BR -> IO a_a5BR
(return $ VG.fromList [(1 :: Int, 2 :: Int), (3, 5)] ::
VProd Vector (Pair Unit Unit) (Int, Int))I then experimented with using Data Families instead
data Prod = Pair Prod Prod | Unit
data family VProd (vect :: * -> * ) (prd:: Prod ) val -- where
data instance VProd v Unit a where
VLeaf :: !(v a) -> VProd v Unit a
data instance VProd v (Pair pra prb ) (a,b) where
VPair :: !(VProd v pra a) -> !(VProd v prb b ) ->VProd v (Pair pra prb) (a,b)
data family MVProd (vect :: * -> * -> * ) (prd:: Prod ) (st :: * ) val -- where
data instance MVProd mv Unit st a where
MVLeaf :: !(mv st a) -> MVProd mv Unit st a
data instance MVProd mv (Pair pra prb) st (a,b) where
MVPair :: !(MVProd mv pra st a) -> !(MVProd mv prb st b ) -> MVProd mv (Pair pra prb) st (a,b)
and type inference would chug along quite happily on the same example.
Attached is the file needed to (somewhat minimally) reproduce this
I guess what I'm saying here is I've quite a funny tension, I'm writing a patently closed data type, which has a perfectly reasonable GADT definition, but I need to use an (Open!) data family definition to get good type inference in the use sites!
This seems like something where (roughly) when the GADT constructors satisfy something analogous to the no overlap condition of a valid data family, similarly strong type inference might be possible? I'm not sure if this makes sense, so i'm posing it as a feature request because i'm Not quite sure what the implications would be within type inference, but it'd probably be quite nice for end users because they'd suddenly get much better type inference for a large class of GADTs (i think)