[GHC] #10204: Odd interaction between rank-2 types and type families

[GHC]

#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