Core Lint error with Type.Reflection and pattern synonyms
{-# 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
.
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 |