GitLab

{-# 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