#16074: Hopelessly confusing error involving runtime-reps -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by simonpj: Old description:

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.

New description: 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. Reported in comment:5 of #16050 -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16074#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16074: Hopelessly confusing error involving runtime-reps -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T16074 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => typecheck/should_fail/T16074 * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16074#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler