[GHC] #9667: Type inference is weaker for GADT than analogous Data Family
#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
#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
#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: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9667#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9667#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Comment (by simonpj): Yes, a reproducible example would be great. Thanks -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9667#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Comment (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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9667#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Comment (by carter): That should load in ghci, and then you can follow the steps in the top level comments to reproduce the problem. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9667#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Comment (by carter): The only dependencies needed are Vector and Primitive packages. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9667#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Comment (by goldfire): The attached file still doesn't seem too minimal to me.... Do we really need all that `basicUnsafe...` stuff? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9667#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9667#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Comment (by carter): I've created a self contained single module repro, attached as the GadtVsData.hs file -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9667#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Comment (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?) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9667#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Comment (by carter): ok, i'll strip it down more. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9667#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Comment (by carter): I managed to boil it down a bit more -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9667#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9667#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC