Opened 5 years ago

Last modified 4 years ago

#9667 new feature request

Type inference is weaker for GADT than analogous Data Family

Reported by: carter Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.3
Keywords: TypeFamilies, GADTs Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by carter)

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)

Attachments (3)

Pair.hs (9.9 KB) - added by carter 5 years ago.
attaching directions to reproduce the inference problem
GadtVsData.hs (7.1 KB) - added by carter 5 years ago.
Gadts vs data fams via small example
SimplerGadtVsData.hs (2.3 KB) - added by carter 5 years ago.
Even Simpler GADT vs Data Families example

Download all attachments as: .zip

Change History (19)

comment:1 Changed 5 years ago by carter

Description: modified (diff)

comment:2 Changed 5 years ago by carter

basically I want something that has the closed-ness of a GADT, and the inferency goodness of a data family. Whether this is a new thing or a "special stronger case of gadt", is another matter i'm happy to try to help someone figure out.

comment:3 Changed 5 years ago by goldfire

Can you create a minimal example? I can't run your example in the original post because it has unstated dependencies, and the attached file has a lot of stuff that's presumably unrelated.

But, it sounds like you want some sort of type-level injectivity guarantee on a GADT. Interesting thought.

comment:4 Changed 5 years ago by simonpj

Yes, a reproducible example would be great. Thanks

comment:5 Changed 5 years ago by carter

oh, looks like i uploaded the wrong Pair.hs file http://lpaste.net/raw/112106 is the correct one, i'll upload that in a jiffy

Changed 5 years ago by carter

Attachment: Pair.hs added

attaching directions to reproduce the inference problem

comment:6 Changed 5 years ago by carter

That should load in ghci, and then you can follow the steps in the top level comments to reproduce the problem.

comment:7 Changed 5 years ago by carter

The only dependencies needed are Vector and Primitive packages.

comment:8 Changed 5 years ago by goldfire

The attached file still doesn't seem too minimal to me.... Do we really need all that basicUnsafe... stuff?

comment:9 Changed 5 years ago by carter

i can replace most of that with stubs that are defined with= error "not defined" if you wanted, might take a bit longer for me to boil down the rest into a more minimal repro, but i'll try to find the time to think about it.

Changed 5 years ago by carter

Attachment: GadtVsData.hs added

Gadts vs data fams via small example

comment:10 Changed 5 years ago by carter

I've created a self contained single module repro, attached as the GadtVsData.hs file

comment:11 Changed 5 years ago by goldfire

Sorry to pester about this, but your example still seems not minimal. I don't think we're looking for a real-world minimal example, just a syntactic one. There seems to be a bunch of things in that file which are not related to this ticket. (All the methods in that class? Strictness annotations?)

comment:12 Changed 5 years ago by carter

ok, i'll strip it down more.

comment:13 Changed 5 years ago by carter

I managed to boil it down a bit more

Changed 5 years ago by carter

Attachment: SimplerGadtVsData.hs added

Even Simpler GADT vs Data Families example

comment:14 Changed 5 years ago by goldfire

Adding the following definitions made this more perspicuous to me:

fromList1DF :: (List l a, List l b) => [(a,b)] -> DFProd l (Pair Unit Unit) (a, b)
fromList1DF [] = DFPair (DFLeaf nil) (DFLeaf nil)
fromList1DF ((a,b):xs) = case fromList1DF xs of
    DFPair (DFLeaf as) (DFLeaf bs) ->
      DFPair (DFLeaf (a `cons` as)) (DFLeaf (b `cons` bs))
                         
fromList1GA :: (List l a, List l b) => [(a,b)] -> GAProd l (Pair Unit Unit) (a, b)
fromList1GA [] = GAPair (GALeaf nil) (GALeaf nil)
fromList1GA ((a,b):xs) = case fromList1GA xs of
    GAPair (GALeaf as) (GALeaf bs) ->
      GAPair (GALeaf (a `cons` as)) (GALeaf (b `cons` bs))
    -- GAPair (GAPair _ _) _ -> undefined
    -- GAPair (GALeaf _) (GAPair _ _) -> undefined
    _ -> error "GADT warnings bad"

(Note that the one pattern in fromList1GA is actually complete, but #3927 bites unless we have the catchall case. The commented-out lines were my tests to make sure that other patterns were indeed inaccessible.)

fromList1DF compiles just fine. fromList1GA fails with two errors, the second being

/Users/rae/temp/bug/SimplerGadtVsData.hs:104:32:
    Couldn't match type ‘l0’ with ‘l’
      ‘l0’ is untouchable
        inside the constraints ('Pair 'Unit 'Unit ~ 'Pair pra prb,
                                (a, b) ~ (a1, b1))
        bound by a pattern with constructor
                   GAPair :: forall (v :: * -> *) (pra :: Prod) a (prb :: Prod) b.
                             GAProd v pra a
                             -> GAProd v prb b -> GAProd v ('Pair pra prb) (a, b),
                 in a case alternative
        at /Users/rae/temp/bug/SimplerGadtVsData.hs:103:5-34
      ‘l’ is a rigid type variable bound by
          the type signature for
            fromList1GA :: (List l a, List l b) =>
                           [(a, b)] -> GAProd l ('Pair 'Unit 'Unit) (a, b)
          at /Users/rae/temp/bug/SimplerGadtVsData.hs:100:16
    Expected type: l a
      Actual type: l0 a1
    Relevant bindings include
      bs :: l0 b1
        (bound at /Users/rae/temp/bug/SimplerGadtVsData.hs:103:32)
      as :: l0 a1
        (bound at /Users/rae/temp/bug/SimplerGadtVsData.hs:103:20)
      fromList1GA :: [(a, b)] -> GAProd l ('Pair 'Unit 'Unit) (a, b)
        (bound at /Users/rae/temp/bug/SimplerGadtVsData.hs:101:1)
    In the second argument of ‘cons’, namely ‘as’
    In the first argument of ‘GALeaf’, namely ‘(a `cons` as)’

(The first is a failure about class constraints. This failure is a direct consequence of the error listed above. Indeed, I would say that the first error -- which complains about ambiguity of l0 -- should be suppressed when we also report that l0 is untouchable.)

The problem is that GHC can't infer the result type of the GADT pattern match. Perhaps this result type somehow depends on the information we learn about pra and prb in the match, and there's no way to infer this dependency. So, GHC gives up -- this is the essence of "untouchable" variables.

I think there is room for improvement here, because the GADT pattern match wasn't actually informative, in this case: all the information that comes out of the match is known beforehand, via the details of the type signature. It is perhaps conceivable to detect this corner case and not make the "global" tyvars become untouchable. I don't know if this is worth pursuing very deeply, but I think that's what's going on.

comment:15 Changed 4 years ago by thomie

Keywords: TypeFamilies added

comment:16 Changed 4 years ago by thomie

Keywords: GADTs added
Note: See TracTickets for help on using tickets.