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

core-dump.log (13.6 KB) - added by Iceland_jack 12 months ago.

Download all attachments as: .zip

Change History (9)

Changed 12 months ago by Iceland_jack

Attachment: core-dump.log added

comment:1 Changed 12 months 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 12 months ago by dobenour

Priority: normalhighest

comment:3 Changed 11 months ago 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!

comment:4 Changed 11 months ago by simonpj

Keywords: TypeInType added

comment:5 Changed 10 months ago by Simon Peyton Jones <simonpj@…>

In 40cbab9a/ghc:

Fix another obscure pattern-synonym crash

This one, discovered by Iceland Jack (Trac #14507), shows
that a pattern-bound coercion can show up in the argument
type(s) of the matcher of a pattern synonym.

The error message isn't great, but at least we now rightly
reject the program.

comment:6 Changed 10 months ago 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.

comment:7 Changed 10 months ago by Iceland_jack

I'm very honored Simon!

comment:8 Changed 10 months ago by simonpj

Resolution: fixed
Status: newclosed
Note: See TracTickets for help on using tickets.