#9269: Type families returning quantified types -------------------------------------+------------------------------------ Reporter: pumpkin | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): It depends on how "fundamental" a reason you want. Consider this: {{{ type family Foo (x :: Bool) where Foo True = forall a. a -> a -> a Foo False = () data SBool :: Bool -> * where STrue :: SBool True SFalse :: SBool False bar :: SBool b -> Foo b -> () bar STrue x = (x 'a' 'b', x True False) `seq` () bar SFalse x = x }}} It seems to be that it would be reasonable to expect the above code to typecheck, if we're allowed to write a family `Foo`. But, getting this to work wreaks havoc with the way GHC's typechecker is built. GHC walks over a term and builds up a set of constraints. For example, if the term is something like `z True`, then GHC will decide that `z` has type `alpha`, for some unknown type `alpha`. Then, it says that we must have `alpha ~ (beta -> gamma)`, from the fact that `z` is in a function position. We then see that `beta ~ Bool` from the type of `True`. After walking over an entire term, GHC then solves these constraints, in this case getting that the type of `z` must be `(Bool -> gamma)`. The crucial problem in the code above is that this algorithm runs into trouble on the RHS of the first clause of `bar`. GHC will see that `x` is used in a function position and will try to infer a type like `alpha -> beta` for `x`, which is dead wrong. "But wait," you say: "GHC can know that `x` should have type `forall a. a -> a -> a` by then!" Well, not quite. GHC knows that `x` has type `Foo b` (from the type signature) and that `b ~ True` (from the GADT pattern-match), but it hasn't yet put those pieces together: that's what the solver does! And, we don't want to try to run the solver before generating all the constraints, because the solver might do the wrong thing when it doesn't have enough information. One possible way forward here is to modify the offending line of the program above as follows: {{{ bar STrue (x :: forall a. a -> a -> a) = ... }}} Now, GHC knows the correct type of `x` on the RHS and can generate constraints there without a problem. When the solver runs, it needs to solve `Foo b ~ forall a. a -> a -> a`, which works out just fine, given the GADT pattern-match. This requirement (the extra type annotation) is strange and unexpected to users, who are likely not thinking about GHC's constraint-solving algorithm. Does this fact make your proposed feature a bad idea? I don't know. And, there may be yet other reasons why what you want is a bad idea; this one is just one possible reason. Do others know of other problems here? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9269#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9269: Type families returning quantified types -------------------------------------+------------------------------------- Reporter: pumpkin | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 11962 Related Tickets: #13901 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) * blocking: => 11962 * related: => #13901 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9269#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9269: Type families returning quantified types -------------------------------------+------------------------------------- Reporter: pumpkin | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 11962 Related Tickets: #13901 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by int-index): * cc: int-index (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9269#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9269: Type families returning quantified types -------------------------------------+------------------------------------- Reporter: pumpkin | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 11962 Related Tickets: #13901 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Tritlo): * cc: Tritlo (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9269#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler