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

#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

#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 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: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): More output: Replacing it with {{{#!hs 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) | ^^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14500#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 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: | -------------------------------------+------------------------------------- Comment (by goldfire): 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.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14500#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 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: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): I do pass `-fprint-explicit-coercions` to ghci so it's wasn't a shock to me to find a coercion :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14500#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 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: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I'm confused. You explicitly pass `-fprint-explicit-coercions`, and lo and behold, coercions appear in error messages. What exactly is the bug here? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14500#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 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: | -------------------------------------+------------------------------------- Comment (by goldfire): 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14500#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 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: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Well, if the name "`cobox`" bothers you, you'll be happy to know that that name is no longer used in GHC HEAD (after 79ae03aa32c277ae93827519ed7738938e3e1572): {{{ $ ~/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) () | ^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14500#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14500: Coercion artifact ‘cobox’ appears in error message -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: invalid | 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => invalid Comment: Closing, as this is working as advertised. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14500#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14500: Coercion artifact ‘cobox’ appears in error message -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: invalid | 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: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Yes, it was confusion on my part -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14500#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC