[GHC] #14500: Coercion artifact ‘cobox’ appears in error message

21 Nov 2017


      #14500: Coercion artifact ‘cobox’ appears in error message
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           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:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# 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.
[https://downloads.haskell.org/~ghc/master/users-guide/using.html#ghc-
 flag--fprint-explicit-coercions GHC User Guide]
-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14500
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler