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

27 Mar 2015

      #10204: Odd interaction between rank-2 types and type families
-------------------------------------+-------------------------------------
              Reporter:  diatchki    |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.10.1
  (Type checker)                     |  Operating System:  Unknown/Multiple
              Keywords:              |   Type of failure:  GHC rejects
          Architecture:              |  valid program
  Unknown/Multiple                   |        Blocked By:
             Test Case:              |   Related Tickets:
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 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`.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10204
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler