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 )
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)
Change History (19)
comment:1 Changed 5 years ago by
Description: | modified (diff) |
---|
comment:2 Changed 5 years ago by
comment:3 Changed 5 years ago by
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:5 Changed 5 years ago by
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
attaching directions to reproduce the inference problem
comment:6 Changed 5 years ago by
That should load in ghci, and then you can follow the steps in the top level comments to reproduce the problem.
comment:8 Changed 5 years ago by
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
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.
comment:10 Changed 5 years ago by
I've created a self contained single module repro, attached as the GadtVsData.hs file
comment:11 Changed 5 years ago by
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?)
Changed 5 years ago by
Attachment: | SimplerGadtVsData.hs added |
---|
Even Simpler GADT vs Data Families example
comment:14 Changed 5 years ago by
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
Keywords: | TypeFamilies added |
---|
comment:16 Changed 4 years ago by
Keywords: | GADTs added |
---|
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.