[GHC] #14570: Untouchable error arises from type equality, but not equivalent program with fundeps

10 Dec 2017

      #14570: Untouchable error arises from type equality, but not equivalent program
with fundeps
-------------------------------------+-------------------------------------
           Reporter:  lexi.lambda    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.2
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Given some type definitions:

 {{{#!hs
 data A
 data B (f :: * -> *)
 data X (k :: *)
 }}}

 …and this typeclass:

 {{{#!hs
 class C k a | k -> a
 }}}

 …these (highly contrived for the purposes of a minimal example) function
 definitions typecheck:

 {{{#!hs
 f :: forall f. (forall k. (C k (B f)) => f k) -> A
 f _ = undefined

 g :: (forall k. (C k (B X)) => X k) -> A
 g = f
 }}}

 However, if we use a type family instead of a class with a functional
 dependency:

 {{{#!hs
 type family F (k :: *)
 }}}

 …then the equivalent function definitions fail to typecheck:

 {{{#!hs
 f :: forall f. (forall k. (F k ~ B f) => f k) -> A
 f _ = undefined

 g :: (forall k. (F k ~ B X) => X k) -> A
 g = f
 }}}

 {{{
 • Couldn't match type ‘f0’ with ‘X’
     ‘f0’ is untouchable
       inside the constraints: F k ~ B f0
       bound by a type expected by the context:
                  F k ~ B f0 => f0 k
   Expected type: f0 k
     Actual type: X k
 • In the expression: f
   In an equation for ‘g’: g = f
 }}}

 I read Section 5.2 of the OutsideIn(X) paper, which describes touchable
 and untouchable type variables, and I ''sort of'' understand what’s going
 on here. If I add an extra argument to `f` that pushes the choice of `f`
 outside the inner `forall`, then the program typechecks:

 {{{#!hs
 f :: forall f a. f a -> (forall k. (F k ~ B f) => f k) -> A
 f _ _ = undefined

 g :: forall a. X a -> (forall k. (F k ~ B X) => X k) -> A
 g = f
 }}}

 I don’t know if this is actually a bug—it seems entirely reasonable to me
 that I don’t fully understand what is going on here—but I’m stumped as to
 ''why'' GHC rejects this program but accepts the one involving functional
 dependencies. I would expect it to either accept or reject both programs,
 given they ''seem'' equivalent.

 Is this just an unfortunate infelicity of the differences between how
 functional dependencies and type equalities are internally solved? Or is
 there a deeper difference between these two programs?

 ,,(Note: This ticket is adapted from
 [https://stackoverflow.com/q/47734825/465378 this Stack Overflow
 question].),,

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