Opened 4 years ago

Last modified 4 years ago

#10204 new feature request

Odd interaction between rank-2 types and type families

Reported by: diatchki Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.10.1
Keywords: TypeFamilies 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 diatchki)

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

{-# 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.

Change History (5)

comment:1 Changed 4 years ago by goldfire

Just to note: this is not a regression for 7.10. The identical behavior appears in 7.8.

comment:2 Changed 4 years ago by diatchki

Description: modified (diff)

comment:3 Changed 4 years ago by diatchki

Description: modified (diff)

comment:4 Changed 4 years ago by simonpj

Milestone:
Type: bugfeature request

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 OutsideIn paper

I'll mark this as a feature request!

Simon

comment:5 Changed 4 years ago by thomie

Keywords: TypeFamilies added
Note: See TracTickets for help on using tickets.