GitLab

{-# 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