[GHC] #9667: Type inference is weaker for GADT than analogous Data Family

4 Oct 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