[GHC] #16074: Hopelessly confusing error involving runtime-reps

[GHC]

#16074: Hopelessly confusing error involving runtime-reps
-------------------------------------+-------------------------------------
           Reporter:  simonpj        |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider
 {{{
 {-# LANGUAGE GADTs, TypeOperators, PolyKinds #-}

 import GHC.Types

 data a :~: b where Refl :: a :~: a

 foo :: TYPE a :~: TYPE b
 foo = Refl
 }}}
 We get
 {{{
     • Couldn't match type ‘'LiftedRep’ with ‘'LiftedRep’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           foo :: * :~: *
         at Repr.hs:7:1-24
       ‘b’ is a rigid type variable bound by
         the type signature for:
           foo :: * :~: *
         at Repr.hs:7:1-24
 }}}
 That's a ridiculous message.  But if you asdd `-fprint-explicit-runtime-
 reps` we get
 {{{
     • Couldn't match type ‘a’ with ‘b’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           foo :: forall (a :: RuntimeRep) (b :: RuntimeRep).
                  TYPE a :~: TYPE b
         at T16050.hs:9:1-24
       ‘b’ is a rigid type variable bound by
         the type signature for:
           foo :: forall (a :: RuntimeRep) (b :: RuntimeRep).
                  TYPE a :~: TYPE b
         at T16050.hs:9:1-24
       Expected type: TYPE a :~: TYPE b
         Actual type: TYPE a :~: TYPE a
     • In the expression: Refl
       In an equation for ‘foo’: foo = Refl
     • Relevant bindings include
         foo :: TYPE a :~: TYPE b (bound at T16050.hs:10:1)
 }}}
 which is the right error.

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