Opened 10 months ago
Closed 9 months ago
#14507 closed bug (fixed)
Core Lint error with Type.Reflection and pattern synonyms
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | highest | Milestone: | |
Component: | Compiler | Version: | 8.2.1 |
Keywords: | PatternSynonyms, TypeInType | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
{-# 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
.
Attachments (1)
Change History (9)
Changed 10 months ago by
Attachment: | core-dump.log added |
---|
comment:1 Changed 10 months ago by
comment:2 Changed 10 months ago by
Priority: | normal → highest |
---|
comment:3 Changed 9 months ago by
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!
comment:4 Changed 9 months ago by
Keywords: | TypeInType added |
---|
comment:6 Changed 9 months ago by
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.
comment:8 Changed 9 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Note: See
TracTickets for help on using
tickets.
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.