[GHC] #11642: Heterogeneous type equality evidence ignored

[GHC]

#11642: Heterogeneous type equality evidence ignored
-------------------------------------+-------------------------------------
        Reporter:  bgamari           |                Owner:  goldfire
            Type:  bug               |               Status:  closed
        Priority:  highest           |            Milestone:  8.0.1
       Component:  Compiler (Type    |              Version:  7.10.3
  checker)                           |
      Resolution:  invalid           |             Keywords:  TypeInType
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:                    |
-------------------------------------+-------------------------------------
Changes (by goldfire):

 * status:  new => closed
 * resolution:   => invalid


Comment:

 A maze this is, indeed. But, happily(?), we humans were the ones lost, not
 GHC, which is spot on.

 The original code is

 {{{#!hs
 buildApp :: TypeRepX -> TypeRepX -> TypeRepX
 buildApp (TypeRepX f) (TypeRepX x) =
   case typeRepKind f of
     TRFun arg _ ->
       case eqTypeRep arg x of
         Just HRefl ->
           TypeRepX $ TypeApp f x
 }}}

 Let me augment with some kinds and such:

 {{{#!hs
 buildApp :: TypeRepX -> TypeRepX -> TypeRepX
 buildApp (TypeRepX f) (TypeRepX x) =
   -- f :: TypeRep kind_tf (tf :: kind_tf)
   -- x :: TypeRep kind_tx (tx :: kind_tx)
   case typeRepKind f of
     TRFun arg _ ->
       -- arg :: TypeRep kind_targ (targ :: kind_targ)
       -- _   :: TypeRep kind_tres (tres :: kind_tres)
       -- _   :: kind_tf ~ (targ -> tres)
       -- _   :: kind_targ ~ *
       -- _   :: kind_tres ~ *
       case eqTypeRep arg x of
         Just HRefl ->
           -- _ :: kind_targ ~ kind_tx   (but kind_targ ~ *)
           -- _ :: targ      ~ tx
           TypeRepX $ TypeApp f x
             -- NEED: exists k1 k2.
             --   kind_tf ~ k1 -> k2
             --   kind_tx ~ k1
 }}}

 At the end, we need to find `k1` and `k2` such that those two equalities
 are provable from our givens. The choice of `k1` and `k2` is quite clear:
 choose `k1 := targ` and `k2 := tres`. Now, we must prove `kind_tx ~ targ`.
 But we can't! We know that `targ ~ tx`, not `targ ~ kind_tx`. Note that,
 actually, `kind_tx` is really known to be `*`. So GHC helpfully reports

 {{{
 T11642.hs:47:30: error:
     • Could not deduce: arg ~ *
       from the context: k ~ (arg -> res)
         bound by a pattern with pattern synonym:
                    TRFun :: forall fun arg res.
                             (fun ~ (arg -> res)) =>
                             TypeRep arg -> TypeRep res -> TypeRep fun,
                  in a case alternative
         at T11642.hs:37:5-15
       or from: (* ~ k1, arg ~ a1)
         bound by a pattern with constructor:
                    HRefl :: forall k2 (a :: k2). a :~~: a,
                  in a case alternative
         at T11642.hs:44:14-18
       ‘arg’ is a rigid type variable bound by
         a pattern with pattern synonym:
           TRFun :: forall fun arg res.
                    (fun ~ (arg -> res)) =>
                    TypeRep arg -> TypeRep res -> TypeRep fun,
         in a case alternative
         at T11642.hs:37:5
       Expected type: TypeRep a
         Actual type: TypeRep a
     • In the first argument of ‘TypeApp’, namely ‘f’
       In the second argument of ‘($)’, namely ‘TypeApp f x’
       In the expression: TypeRepX $ TypeApp f x
     • Relevant bindings include
         arg :: TypeRep arg (bound at T11642.hs:37:11)
 }}}

 Which is absolutely correct.

 Happily, fixing the code is easy:

 {{{#!hs
 -- ...
       case eqTypeRep arg (typeRepKind x) of
 -- ...
 }}}

 works like a charm.

 I do believe some intermediate work (between when this was reported and
 now) has improved this message. It's still not great, given that it took
 me the better part of an hour to deduce all of the above. But I don't see
 how we can do better without giving the user the trail of breadcrumbs that
 GHC used to find its result. (I ''do'' think we should give this ability
 to the user, somehow. It would be easy enough to implement -- just augment
 `CtLoc` to keep track of previous constraints and how they were
 transformed. The data is all there.)

 I'm thus closing this as invalid. I'm also not adding a regression test,
 because I'm not thrilled with the error message as it is, and there's no
 other unusual behavior here.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11642#comment:10>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler