#10204: Odd interaction between rank-2 types and type families -------------------------------------+------------------------------------- Reporter: diatchki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Description changed by diatchki: Old description:

Type inference does work as expected, when a rank-2 type has type-family constraint. Consider the following program:

{{{#!hs {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE Rank2Types #-}

type family F a

f :: (forall s. (F s ~ Int) => s -> b) -> b f _ = undefined

k :: s -> Char k = undefined

example :: Bool example = const True (f k) }}}

It is rejected with the following error:

{{{ Couldn't match type ‘b0’ with ‘Char’ ‘b0’ is untouchable inside the constraints (F s ~ Int) bound by a type expected by the context: (F s ~ Int) => s -> b0 at bug.hs:13:23-25 Expected type: s -> b0 Actual type: s -> Char In the first argument of ‘f’, namely ‘k’ In the second argument of ‘const’, namely ‘(f k)’ }}}

This is unexpected because the result of `f` should be the same as the result of its parameter, and we know the exact type of the parameter, namely `Char`.

New description: Type inference does not work as expected, when a rank-2 type has type- family constraint. Consider the following program: {{{#!hs {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE Rank2Types #-} type family F a f :: (forall s. (F s ~ Int) => s -> b) -> b f _ = undefined k :: s -> Char k = undefined example :: Bool example = const True (f k) }}} It is rejected with the following error: {{{ Couldn't match type ‘b0’ with ‘Char’ ‘b0’ is untouchable inside the constraints (F s ~ Int) bound by a type expected by the context: (F s ~ Int) => s -> b0 at bug.hs:13:23-25 Expected type: s -> b0 Actual type: s -> Char In the first argument of ‘f’, namely ‘k’ In the second argument of ‘const’, namely ‘(f k)’ }}} This is unexpected because the result of `f` should be the same as the result of its parameter, and we know the exact type of the parameter, namely `Char`. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10204#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10204: Odd interaction between rank-2 types and type families -------------------------------------+------------------------------------- Reporter: diatchki | Owner: Type: feature request | Status: new Priority: normal | Milestone: ⊥ Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Changes (by simonpj): * type: bug => feature request * milestone: => ⊥ Comment: You could indeed consider this a failure of inference, but it's by-design (currently), and it's one I don't know how to fix. Consider this constraint that arise from `example`: {{{ forall s. (F s ~ Int) => (s -> beta) ~ (sigma ~ Char) }}} Here * `beta` is a unification variable that arises from instantiating `b` in the call to `f`. * `sigma` is a unification variable that arises from instantiating `s` in the call to `k`. We can safely unify `sigma := s`, because the call to `k` is inside the polymorphic argument to `f`. But it is less clear that we can unify `beta := Char` because both (a) it affects the inferred type of `(f k)`, and (b) the `(beta ~ Char)` is under an equality `F s ~ Int`.. Suppose that instead of `F s ~ Int` it had been `F s ~ Char`. Then should we unify `beta := Char` or `beta := F s`? GHC never guesses,so instead it refrains from unifying `beta`, saying that it is "untouchable", hoping that some other constraint will determine how to unify `beta`. You may say that `(F s ~ Int)` can't possibly affect `beta`, but it should be clear that it's ''really'' hard to be sure about that. GHC simply treats ''any'' equality in an implication constraint as making all the unification variables from an outer scope untouchable. This issue is discussed (somewhat) in 5.6.1 of the [https://wiki.haskell.org/Simonpj/Talk:OutsideIn OutsideIn paper] I'll mark this as a feature request! Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10204#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler