#15009: Float equalities past local equalities -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: 8.4.3 Component: Compiler | Version: 8.2.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider the two datatypes {{{#!hs data T1 a where MkT1 :: a ~ b => b -> T1 a data T2 a where MkT2 :: a -> T2 a }}} To me, these look like two ways of writing the same thing. Yet they participate quite differently in type inference. If I say {{{#!hs f (MkT1 a) = not a g (MkT2 a) = not a }}} then `g` is accepted (with type `T2 Bool -> Bool`) while `f` is rejected as GHC mutters about untouchable type variables. Of course, GHC's notion of untouchable type variables is a Good Thing, with arguments I won't rehearse here. It all boils down to this rule: (*) Information that arises in the context of an equality constraint cannot force unification of a unification variable born outside that context. I think this rule is a bit too strict, though. I propose a new rule: (%) Information that arises in the context of a ''non-purely-local'' equality constraint cannot force unification of a unification variable born outside that context. where '''Definition:''' An equality constraint is ''purely local'' if every type variable free in the constraint has the same scope as the constraint itself. That is, if an equality constraint mentions only variables freshly brought into scope -- and no others -- then we can still unify outer unification variables. Happy consequences of this choice: * `f` above could be accepted, as the equality in `MkT1` is purely local. * Rule (%) allows users to effectively let-bind type variables, like this: {{{#!hs f :: forall a. (a ~ SOME REALLY LONG TYPE) => Maybe a -> Maybe a -> Either a a }}} Currently, this kind of definition (if it's, say, within a `where` clause) triggers rule (*) in the body of the function, and thus causes type inference to produce a different result than just inlining `SOME REALLY LONG TYPE`. * We could theoretically simplify our treatment of GADTs. Right now, if you say {{{#!hs data G a b c where MkG :: MkG d Int [e] }}} GHC has to cleverly figure out that `d` is a universal variable and that `e` is an existential, producing the following Core: {{{#!hs data G a b c where MkG :: forall d b c. forall e. (b ~ Int, c ~ [e]) => MkG d b c }}} If we use rule (%), then I believe the following Core would behave identically: {{{#!hs data G a b c where MkG :: forall a b c. forall d e. (a ~ d, b ~ Int, c ~ [e]). MkG a b c }}} This treatment is more uniform and easier to implement. (Note that the equality constraints themselves are unboxed, so there's no change in runtime performance.) What are the downsides of (%)? I don't think there are any, save an easy extra line or two in GHC to check for locality. Rule (*) exists because, without it, GHC can infer non-principal types. However, I conjecture that Rule (%) also serves to require inference of only principal types, while being more permissive than Rule (*). I'm curious for your thoughts on this proposal. (I am making it here, as this is really an implementation concern, with no discernible effect on, say, the user manual, although it would allow GHC to accept more programs.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15009 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler