[GHC] #9667: Type inference is weaker for GADT than analogous Data Family
GHC
ghc-devs at haskell.org
Sun Oct 5 00:44:34 UTC 2014
#9667: Type inference is weaker for GADT than analogous Data Family
-------------------------------------+-------------------------------------
Reporter: carter | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 7.8.3
checker) | Operating System:
Keywords: | Unknown/Multiple
Architecture: Unknown/Multiple | Type of failure: GHC
Difficulty: Unknown | rejects valid program
Blocked By: | Test Case:
Related Tickets: | Blocking:
| Differential Revisions:
-------------------------------------+-------------------------------------
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
{{{#!hs
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
{{[#!hs
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)
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9667>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list