[GHC] #14507: Core Lint error with Type.Reflection and pattern synonyms
#14507: Core Lint error with Type.Reflection and pattern synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple PatternSynonyms | 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, TypeFamilies, TypeFamilyDependencies #-} import Type.Reflection import Prelude import Data.Kind data Dict c where Dict :: c => Dict c data N = O | S N foo :: forall (kind::k') (a::k). TypeRep kind -> TypeRep a -> Maybe (kind :~~: k, TypeRep a) foo krep rep = do HRefl <- eqTypeRep krep (typeRepKind rep) pure (HRefl, rep) 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)) where Bloop' HRefl rep = rep type family SING = (res :: k -> Type) | res -> k where -- Core Lint error disappears with this line: SING = (TypeRep :: N -> Type) pattern RepN :: forall (a::kk). Typeable a => N~kk => SING a -> TypeRep (a::kk) pattern RepN tr <- Bloop' (HRefl::N:~~:kk) (tr :: TypeRep (a::N)) where RepN tr = tr asTypeable :: TypeRep a -> Dict (Typeable a) asTypeable rep = withTypeable rep Dict pattern TypeRep :: () => Typeable a => TypeRep a pattern TypeRep <- (asTypeable -> Dict) where TypeRep = typeRep -- error pattern SO = RepN TypeRep }}} triggers “Core Lint errors” on 8.2.1, 8.3.20170920 when run with `ghci -ignore-dot-ghci -dcore-lint`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14507 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14507: Core Lint error with Type.Reflection and pattern synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: | PatternSynonyms 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 Iceland_jack): * Attachment "core-dump.log" added. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14507 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14507: Core Lint error with Type.Reflection and pattern synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: | PatternSynonyms 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 dobenour): You should ''never'' get a failure in Core Lint, so this is definitely a bug. Moving to highest priority. This is obviously a bug in either the type checker or the desugarer. Either the type checker is accepting garbage or the desugarer is messing up. My instinct says to blame the desugarer – a type variable out of scope doesn’t make any sense at all. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14507#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14507: Core Lint error with Type.Reflection and pattern synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: | PatternSynonyms 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 dobenour): * priority: normal => highest -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14507#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14507: Core Lint error with Type.Reflection and pattern synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: | PatternSynonyms 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 simonpj): Here's a smaller example {{{ module T14507 where import Type.Reflection import Data.Kind foo :: TypeRep a -> (Bool :~~: k, TypeRep a) foo rep = error "urk" type family SING :: k -> Type where -- Core Lint error disappears with this line: SING = (TypeRep :: Bool -> Type) pattern RepN :: forall (a::kk). () => Bool~kk => SING a -> TypeRep (a::kk) pattern RepN tr <- (foo -> ( HRefl :: Bool:~~:kk , tr :: TypeRep (a::Bool))) -- error pattern SO x <- RepN (id -> x) }}} The trouble is that the matcher for `SO` has a type like this {{{ $mSO :: forall (r :: TYPE rep) kk (a :: kk). TypeRep kk a -> (((Bool :: *) ~ (kk :: *)) => TypeRep Bool (a |> co_a2sv) -> r) -> (Void# -> r) -> r }}} where that unbound `co_a2sv` actually a coercion derived from the match on `(Bool ~ kk)`. If you like, the real second (continuation) argument of `$msO` is more like {{{ -> (forall (co::Bool~kk) -> TypeRep Bool (a |> get-superclass co) -> r }}} This is bogus because * We don't have term-level dependency `forall co -> ...` * We can't extract a superclass in a type. Richard, I need your help again! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14507#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14507: Core Lint error with Type.Reflection and pattern synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: | PatternSynonyms, TypeInType 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 simonpj): * keywords: PatternSynonyms => PatternSynonyms, TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14507#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14507: Core Lint error with Type.Reflection and pattern synonyms
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: new
Priority: highest | Milestone:
Component: Compiler | Version: 8.2.1
Resolution: | Keywords:
| PatternSynonyms, TypeInType
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 Simon Peyton Jones
#14507: Core Lint error with Type.Reflection and pattern synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: | PatternSynonyms, TypeInType 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 simonpj): OK now we just reject this program with this error message {{{ T14507.hs:19:9: error: • Iceland Jack! Iceland Jack! Stop torturing me! Pattern-bound variable x :: TypeRep a has a type that mentions pattern-bound coercion: co_a2CF Hint: use -fprint-explicit-coercions to see the coercions Probable fix: add a pattern signature • In the declaration for pattern synonym ‘SO’ }}} I hope you don't mind being immoralised in an error message. If you do, just say and I'll remove it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14507#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14507: Core Lint error with Type.Reflection and pattern synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: | PatternSynonyms, TypeInType 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'm very honored Simon! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14507#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14507: Core Lint error with Type.Reflection and pattern synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: highest | Milestone: Component: Compiler | Version: 8.2.1 Resolution: fixed | Keywords: | PatternSynonyms, TypeInType 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 simonpj): * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14507#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC