Coercion artifact ‘cobox’ appears in error message

{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds, TypeInType, TypeOperators, TypeApplications #-}

import Type.Reflection

foo :: forall (kind::k') (a::k). TypeRep kind -> TypeRep a -> Maybe (kind :~~: k, TypeRep a)
foo krep rep = undefined 

data N = O | S N

pattern Bloop' :: forall k' (a::k). Typeable k' => k':~~:k -> TypeRep (a::k) -> TypeRep (a::k)
pattern Bloop' hrefl rep <- (foo (typeRep @k') -> Just (hrefl, rep))

pattern SO :: forall (a::kk). () => N~kk => TypeRep (a::kk)
pattern SO <- Bloop' (HRefl::N:~~:kk) ()

Coercion artifact cobox appears in the error message

$ ghci -ignore-dot-ghci -fprint-explicit-coercions /tmp/Bug.hs 
GHCi, version 8.3.20170920: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /tmp/Bug.hs, interpreted )

/tmp/Bug.hs:14:39: error:
    • Couldn't match type ‘()’ with ‘TypeRep (a |> cobox)’
      Expected type: TypeRep a
        Actual type: ()
    • In the pattern: ()
      In the pattern: Bloop' (HRefl :: N :~~: kk) ()
      In the declaration for pattern synonym ‘SO’
   |
14 | pattern SO <- Bloop' (HRefl::N:~~:kk) ()
   |                                       ^^
Failed, 0 modules loaded.
Prelude> 

This may be intentional but the user guide says they are meant to be internal, so I'm double checking.

Using -fprint-explicit-coercions makes GHC print coercions in types. When trying to prove the equality between types of different kinds, GHC uses type-level coercions. Users will rarely need to see these, as they are meant to be internal.

GHC User Guide

Trac metadata

Trac field	Value
Version	8.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

More output: Replacing it with

pattern SO <- Bloop' (HRefl::N:~~:kk) (typeRep :: TypeRep O)

gives

/tmp/Bug.hs:14:40: error:
    • Could not deduce: a ~ ('O |> Sym cobox)
      from the context: (* ~ *, kk ~ N)
        bound by a pattern with constructor:
                   HRefl :: forall k1 (a :: k1). a :~~: a,
                 in a pattern synonym declaration
        at /tmp/Bug.hs:14:23-27
      ‘a’ is a rigid type variable bound by
        the signature for pattern synonym ‘SO’ at /tmp/Bug.hs:13:23
      Expected type: TypeRep a
        Actual type: TypeRep 'O
    • When checking that the pattern signature: TypeRep 'O
        fits the type of its context: TypeRep a
      In the pattern: typeRep :: TypeRep O
      In the pattern: Bloop' (HRefl :: N :~~: kk) (typeRep :: TypeRep O)
   |
14 | pattern SO <- Bloop' (HRefl::N:~~:kk) (typeRep::TypeRep O)
   |                                        ^^^^^^^^^^^^^^^^^^

(I don't expect these examples to compile)

That's very odd. Are you sure you don't have -fprint-explicit-coercions on? (I don't have a good GHC to test with at the moment.)

I do pass -fprint-explicit-coercions to ghci so it's wasn't a shock to me to find a coercion :)

I'm confused. You explicitly pass -fprint-explicit-coercions, and lo and behold, coercions appear in error messages. What exactly is the bug here?

Perhaps you're disturbed by the name cobox? But how is that any worse than the a and t type variables that GHC routinely comes up with?

Well, if the name "cobox" bothers you, you'll be happy to know that that name is no longer used in GHC HEAD (after 79ae03aa):

$ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs -fprint-explicit-coercions
GHCi, version 8.3.20171118: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:14:39: error:
    • Couldn't match type ‘()’ with ‘TypeRep (a |> co)’
      Expected type: TypeRep a
        Actual type: ()
    • In the pattern: ()
      In the pattern: Bloop' (HRefl :: N :~~: kk) ()
      In the declaration for pattern synonym ‘SO’
   |
14 | pattern SO <- Bloop' (HRefl::N:~~:kk) ()
   |                                       ^^

closed

Closing, as this is working as advertised.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid

Yes, it was confusion on my part

added Pnormal label