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

30 Mar 2015

      #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 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`.
New description:

 Type inference does not work as expected, when a rank-2 type has a 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:3
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler