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