Opened 3 weeks ago

Last modified 3 weeks ago

#14507 new bug

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 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)

core-dump.log (13.6 KB) - added by Iceland_jack 3 weeks ago.

Download all attachments as: .zip

Change History (3)

Changed 3 weeks ago by Iceland_jack

Attachment: core-dump.log added

comment:1 Changed 3 weeks ago 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.

comment:2 Changed 3 weeks ago by dobenour

Priority: normalhighest
Note: See TracTickets for help on using tickets.