Opened 4 months ago

Last modified 2 months ago

#15549 new bug

Core Lint error with EmptyCase

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.4.3
Keywords: TypeFamilies, TypeInType Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case:
Blocked By: Blocking:
Related Tickets: #14729 Differential Rev(s):
Wiki Page:

Description

The following program gives a Core Lint error on GHC 8.2.2 and later:

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Kind
import Data.Void

data family Sing (a :: k)

data V1 :: Type -> Type
data instance Sing (z :: V1 p)

class Generic a where
  type Rep a :: Type -> Type
  to :: Rep a x -> a

class PGeneric a where
  type To (z :: Rep a x) :: a

class SGeneric a where
  sTo :: forall x (r :: Rep a x). Sing r -> Sing (To r :: a)

-----

instance Generic Void where
  type Rep Void = V1
  to x = case x of {}

type family EmptyCase (a :: j) :: k where

instance PGeneric Void where
  type To x = EmptyCase x

instance SGeneric Void where
  sTo x = case x of
$ /opt/ghc/8.4.3/bin/ghc Bug.hs -dcore-lint -fforce-recomp       
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
Bug.hs:38:7: warning:
    [in body of lambda with binder x_aZ8 :: Sing r_a12q]
    Kind application error in
      coercion ‘(Sing (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R’
      Function kind = forall k. k -> *
      Arg kinds = [(V1 x_a12p, *), (r_a12q, Rep Void x_a12p)]
    Fun: V1 x_a12p
         (r_a12q, Rep Void x_a12p)
Bug.hs:38:7: warning:
    [in body of lambda with binder x_aZ8 :: Sing r_a12q]
    Kind application error in
      coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’
      Function kind = V1 x_a12p -> *
      Arg kinds = [(r_a12q, Rep Void x_a12p)]
    Fun: V1 x_a12p
         (r_a12q, Rep Void x_a12p)
Bug.hs:38:7: warning:
    [in body of lambda with binder x_aZ8 :: Sing r_a12q]
    Kind application error in
      coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’
      Function kind = V1 x_a12p -> *
      Arg kinds = [(r_a12q, Rep Void x_a12p)]
    Fun: V1 x_a12p
         (r_a12q, Rep Void x_a12p)
<no location info>: warning:
    In the type ‘R:SingV1z x_a12p r_a12q’
    Kind application error in type ‘R:SingV1z x_a12p r_a12q’
      Function kind = forall p -> V1 p -> *
      Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]
    Fun: V1 x_a12p
         (r_a12q, Rep Void x_a12p)
<no location info>: warning:
    In the type ‘R:SingV1z x_a12p r_a12q’
    Kind application error in type ‘R:SingV1z x_a12p r_a12q’
      Function kind = forall p -> V1 p -> *
      Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]
    Fun: V1 x_a12p
         (r_a12q, Rep Void x_a12p)
*** Offending Program ***

<elided>

$csTo_a12n :: forall x (r :: Rep Void x). Sing r -> Sing (To r)
[LclId,
 Arity=1,
 Str=<L,U>x,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
$csTo_a12n
  = \ (@ x_a12p)
      (@ (r_a12q :: Rep Void x_a12p))
      (x_aZ8 :: Sing r_a12q) ->
      case x_aZ8
           `cast` ((Sing
                      (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R ; D:R:SingV1z0[0]
                                                                      <x_a12p>_N <r_a12q>_N
                   :: (Sing r_a12q :: *) ~R# (R:SingV1z x_a12p r_a12q :: *))
      of nt_s13T {
      }

GHC 8.0.2 does not appear to suffer from this Core Lint error.

Change History (6)

comment:1 Changed 4 months ago by RyanGlScott

Summary: Core Lint error with empty closed type familyCore Lint error with EmptyCase

Never mind, empty closed type families have nothing to do with this. Here's an even more minimal way to reproduce the Core Lint error:

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Proxy
import Data.Void

data family Sing (a :: k)
data instance Sing (z :: Void)

type family Rep a
class SGeneric a where
  sTo :: forall (r :: Rep a). Sing r -> Proxy a

type instance Rep Void = Void
instance SGeneric Void where
  sTo x = case x of
$ /opt/ghc/8.4.3/bin/ghc Bug.hs -dcore-lint
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
Bug.hs:19:7: warning:
    [in body of lambda with binder x_ayn :: Sing r_azJ]
    Kind application error in
      coercion ‘(Sing (D:R:RepVoid[0]) <r_azJ>_N)_R’
      Function kind = forall k. k -> *
      Arg kinds = [(Void, *), (r_azJ, Rep Void)]
    Fun: Void
         (r_azJ, Rep Void)
Bug.hs:19:7: warning:
    [in body of lambda with binder x_ayn :: Sing r_azJ]
    Kind application error in coercion ‘D:R:SingVoidz0[0] <r_azJ>_N’
      Function kind = Void -> *
      Arg kinds = [(r_azJ, Rep Void)]
    Fun: Void
         (r_azJ, Rep Void)
Bug.hs:19:7: warning:
    [in body of lambda with binder x_ayn :: Sing r_azJ]
    Kind application error in coercion ‘D:R:SingVoidz0[0] <r_azJ>_N’
      Function kind = Void -> *
      Arg kinds = [(r_azJ, Rep Void)]
    Fun: Void
         (r_azJ, Rep Void)
<no location info>: warning:
    In the type ‘R:SingVoidz r_azJ’
    Kind application error in type ‘R:SingVoidz r_azJ’
      Function kind = Void -> *
      Arg kinds = [(r_azJ, Rep Void)]
    Fun: Void
         (r_azJ, Rep Void)
<no location info>: warning:
    In the type ‘R:SingVoidz r_azJ’
    Kind application error in type ‘R:SingVoidz r_azJ’
      Function kind = Void -> *
      Arg kinds = [(r_azJ, Rep Void)]
    Fun: Void
         (r_azJ, Rep Void)
*** Offending Program ***
$csTo_azH :: forall (r :: Rep Void). Sing r -> Proxy Void
[LclId,
 Arity=1,
 Str=<L,U>x,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
$csTo_azH
  = \ (@ (r_azJ :: Rep Void)) (x_ayn :: Sing r_azJ) ->
      case x_ayn
           `cast` ((Sing
                      (D:R:RepVoid[0]) <r_azJ>_N)_R ; D:R:SingVoidz0[0] <r_azJ>_N
                   :: (Sing r_azJ :: *) ~R# (R:SingVoidz r_azJ :: *))
      of nt_s14C {
      }

However, EmptyCase does appear to play an important role. If I change the implementation of sTo to this:

instance SGeneric Void where
  sTo x = x `seq` undefined

Then the Core Lint error goes away, and the generated Core for sTo instead becomes:

$csTo_r2IT :: forall (r :: Rep Void). Sing r -> Proxy Void
[GblId, Arity=1, Caf=NoCafRefs]
$csTo_r2IT
  = \ (@ (r_a1F4 :: Rep Void)) (x_X1DH :: Sing r_a1F4) ->
      break<0>(x_X1DH)
      case x_X1DH
           `cast` ((Sing
                      (Bug.D:R:RepVoid[0])
                      (Sym (Coh <r_a1F4>_N
                                (Bug.D:R:RepVoid[0]))))_R ; Bug.D:R:SingVoidz0[0] (Sym (Coh (Sym (Coh <r_a1F4>_N
                                                                                                      (Bug.D:R:RepVoid[0])))
                                                                                            (Bug.D:R:RepVoid[0])))
                   :: (Sing r_a1F4 :: *)
                      ~R# (Bug.R:SingVoidz (r_a1F4 |> Bug.D:R:RepVoid[0]) :: *))
      of {
      }

comment:2 Changed 4 months ago by RyanGlScott

Cc: goldfire added

The culprit here appears to be improveSeq. In particular, in its use of topNormaliseType_maybe:

improveSeq :: (FamInstEnv, FamInstEnv) -> SimplEnv
           -> OutExpr -> InId -> OutId -> [InAlt]
           -> SimplM (SimplEnv, OutExpr, OutId)
-- Note [Improving seq]
improveSeq fam_envs env scrut case_bndr case_bndr1 [(DEFAULT,_,_)]
  | Just (co, ty2) <- topNormaliseType_maybe fam_envs (idType case_bndr1)
  = do { case_bndr2 <- newId (fsLit "nt") ty2
        ; let rhs  = DoneEx (Var case_bndr2 `Cast` mkSymCo co) Nothing
              env2 = extendIdSubst env case_bndr rhs
        ; return (env2, scrut `Cast` co, case_bndr2) }

In the program in comment:1, scrut is x (from sTo), and idType case_bndr1 is Sing (Rep Void) r (where (r :: Rep Void)). It's topNormaliseType_maybe's job to reduce the two type families in Sing (Rep Void) r (in particular, Rep Void ~# Void and then Sing Void ~# R:SingVoidz) and return the coercion that witnesses this reduction. However, it appears to produce an entirely bogus coercion:

Sing (D:R:RepVoid[0]) <r>_N)_R ; D:R:SingVoidz0[0] <r>_N
  :: (Sing (Rep Void) r) ~R# (R:SingVoidz r)

Why is this bogus? Because in the axiom D:R:SingVoidz0[0], we have:

COERCION AXIOMS
  axiom Bug.D:R:SingVoidz0 ::
    forall {z :: Void}.
      Sing Void z = Bug.R:SingVoidz -- Defined at ../Bug.hs:11:15

Notice that the argument to D:R:SingVoidz0[0] is of type Void, but in the coercion above, we're giving it r as an argument, which is of type Rep Void, not Void! Unsurprisingly, utter pandemonium ensues when Core Lint inspects this garbage.

The proper coercion would be something like what the second program in comment:1 produces:

(Sing (D:R:RepVoid[0]) (GRefl nominal r (D:R:RepVoid[0])))_R ; D:R:SingVoidz0[0] <(r |> D:R:RepVoid[0])>_N
  :: (Sing (Rep Void) r :: *) ~R# (R:SingVoidz (r |> D:R:RepVoid[0]) :: *)

Alas, topNormaliseType_maybe doesn't produce this. goldfire, do you think the reason that this doesn't happen is due to the same underlying reasons as in #14729? I strongly suspect that this is the case, since I tried calling normaliseType on Sing (Rep Void) r, and it produces the same bogus coercion that topNormaliseType_maybe did.

comment:3 Changed 4 months ago by goldfire

Yes, this looks like #14729.

comment:4 Changed 4 months ago by RyanGlScott

comment:5 Changed 4 months ago by RyanGlScott

Milestone: 8.6.18.8.1

comment:6 Changed 2 months ago by RyanGlScott

Another program, identified in https://ghc.haskell.org/trac/ghc/ticket/15725#comment:7, which may suffer from the same problems as described in this ticket:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}

module Bug where

import Data.Kind (Type)

newtype Identity a = Identity a
newtype Par1 a = Par1 a

data family Sing :: forall k. k -> Type
data instance Sing :: forall k. k -> Type

type family Rep1 (f :: Type -> Type) :: Type -> Type
type instance Rep1 Identity = Par1

type family From1 (z :: f a) :: Rep1 f a
type instance From1 ('Identity x) = 'Par1 x

und :: a
und = und

f :: forall (a :: Type) (x :: Identity a).  Sing x
f = g
    where g :: forall (a :: Type) (f :: Type -> Type) (x :: f a). Sing x
          g = seq (und :: Sing (From1 x)) und
*** Core Lint errors : in result of Simplifier ***
Bug.hs:25:1: warning:
    [in body of lambda with binder x_a19R :: Identity a_a19Q]
    Kind application error in
      coercion ‘(Sing
                   (D:R:Rep1Identity[0] <a_a19Q>_N) <From1 x_a19R>_N)_R’
      Function kind = forall k. k -> *
      Arg kinds = [(Par1 a_a19Q, *),
                   (From1 x_a19R, Rep1 Identity a_a19Q)]
    Fun: Par1 a_a19Q
         (From1 x_a19R, Rep1 Identity a_a19Q)
Bug.hs:25:1: warning:
    [in body of lambda with binder x_a19R :: Identity a_a19Q]
    Kind application error in
      coercion ‘D:R:Singk0[0] <Par1 a_a19Q>_N <From1 x_a19R>_N’
      Function kind = Par1 a_a19Q -> *
      Arg kinds = [(From1 x_a19R, Rep1 Identity a_a19Q)]
    Fun: Par1 a_a19Q
         (From1 x_a19R, Rep1 Identity a_a19Q)
Bug.hs:25:1: warning:
    [in body of lambda with binder x_a19R :: Identity a_a19Q]
    Kind application error in
      coercion ‘D:R:Singk0[0] <Par1 a_a19Q>_N <From1 x_a19R>_N’
      Function kind = Par1 a_a19Q -> *
      Arg kinds = [(From1 x_a19R, Rep1 Identity a_a19Q)]
    Fun: Par1 a_a19Q
         (From1 x_a19R, Rep1 Identity a_a19Q)
<no location info>: warning:
    In the type ‘R:Singk (Par1 a_a19Q) (From1 x_a19R)’
    Kind application error in
      type ‘R:Singk (Par1 a_a19Q) (From1 x_a19R)’
      Function kind = forall k -> k -> *
      Arg kinds = [(Par1 a_a19Q, *),
                   (From1 x_a19R, Rep1 Identity a_a19Q)]
    Fun: Par1 a_a19Q
         (From1 x_a19R, Rep1 Identity a_a19Q)
<no location info>: warning:
    In the type ‘R:Singk (Par1 a_a19Q) (From1 x_a19R)’
    Kind application error in
      type ‘R:Singk (Par1 a_a19Q) (From1 x_a19R)’
      Function kind = forall k -> k -> *
      Arg kinds = [(Par1 a_a19Q, *),
                   (From1 x_a19R, Rep1 Identity a_a19Q)]
    Fun: Par1 a_a19Q
         (From1 x_a19R, Rep1 Identity a_a19Q)
Note: See TracTickets for help on using tickets.