Opened 3 months ago

Closed 2 months ago

#14162 closed bug (fixed)

Core Lint error

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.2.2
Component: Compiler Version: 8.2.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_compile/T14162
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by Iceland_jack)

{-# Options_GHC -dcore-lint #-}

{-# Language TypeOperators, KindSignatures, DataKinds, PolyKinds, TypeFamilies, GADTs, TypeInType #-}

import Data.Kind

data family Sing (a :: k)

data 
  SubList :: [a] -> [a] -> Type where
  SubNil :: SubList '[] '[]
  Keep :: SubList xs ys -> SubList (x ': xs) (x ': ys)
  Drop :: SubList xs ys -> SubList xs (x ': ys)

data instance 
  Sing (x :: SubList ys xs) where
  SSubNil :: Sing SubNil
  SKeep   :: Sing x -> Sing (Keep x)
  SDrop   :: Sing x -> Sing (Drop x)

running it gives a massive core lint error, attached as lint.log.

Attachments (1)

lint.log (22.2 KB) - added by Iceland_jack 3 months ago.

Download all attachments as: .zip

Change History (9)

Changed 3 months ago by Iceland_jack

Attachment: lint.log added

comment:1 Changed 3 months ago by Iceland_jack

From trying to compile Richard's Effects.hs with -dcore-lint.

comment:2 Changed 3 months ago by Iceland_jack

Description: modified (diff)

comment:3 Changed 3 months ago by simonpj

Here's a simpler version

{-# Language TypeOperators, KindSignatures, DataKinds, PolyKinds, TypeFamilies, GADTs, TypeInType #-}

module T14162 where

import Data.Kind

data SubList :: Maybe a -> Type where
  SubNil :: SubList 'Nothing

data family Sing (a :: k)

data instance Sing (x :: SubList ys) where
  SSubNil :: Sing SubNil

There's an ASSERT error in substTy too, if you compile with a -DDEBUG compiler

comment:4 Changed 3 months ago by simonpj

But the actual error is somewhere in the unfolding wrapper for SSubNil, which is injected by CorePrep and looks like this

SSubNil
  :: forall a (ys :: Maybe a) (x :: SubList a ys).
     ((ys :: Maybe a) ~# ('Nothing a :: Maybe a),
      (x :: SubList a ys) ~# ('SubNil a :: SubList a ('Nothing a))) =>
     R:SingSubListx a ys x
[GblId[DataCon],
 Arity=2,
 Caf=NoCafRefs,
 Str=<L,U><L,U>m,
 Unf=OtherCon []]
SSubNil
  = \ (@ a_aSK)
      (@ (ys_aRV :: Maybe a_aSK))
      (@ (x_aRW :: SubList a_aSK ys_aRV))
      (eta_B2
         :: (ys_aRV :: Maybe a_aSK) ~# ('Nothing a_aSK :: Maybe a_aSK))
      (eta_B1
         :: (x_aRW :: SubList a_aSK ys_aRV)
            ~# ('SubNil a_aSK :: SubList a_aSK ('Nothing a_aSK))) ->
      SSubNil
        @ a_aSK
        @ ys_aRV
        @ x_aRW
        @~ (eta_B2
            :: (ys_aRV :: Maybe a_aSK) ~# ('Nothing a_aSK :: Maybe a_aSK))
        @~ (eta_B1
            :: (x_aRW :: SubList a_aSK ys_aRV)
               ~# ('SubNil a_aSK :: SubList a_aSK ('Nothing a_aSK)))

Lint says

*** Core Lint errors : in result of CorePrep ***
<no location info>: warning:
    In the type ‘forall a (ys :: Maybe a) (x :: SubList a ys).
                 ((ys :: Maybe a) ~# ('Nothing a :: Maybe a),
                  (x :: SubList a ys) ~# ('SubNil a :: SubList a ('Nothing a))) =>
                 R:SingSubListx a ys x’
    Kind application error in type ‘SubList a_aSK ys_aRV’
      Function kind = forall {a}. Maybe a -> *
      Arg kinds = [(a_aSK, *), (ys_aRV, Maybe a_aSv)]

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

In 3a27e34/ghc:

Fix subtle bug in TcTyClsDecls.mkGADTVars

This bug was revealed by Trac #14162.  In a GADT-style data-family
instance we ended up a data constructor whose type mentioned
an out-of-scope variable.  (This variable was in the kind of
a variable in the kind of a variable.)

Only Lint complained about this (actually only when the
data constructor was injected into the bindings by CorePrep).
So it doesn't matter much -- but it's a solid bug and might
bite us some day.

It took me quite a while to unravel because the test case was itself
quite tricky.  But the fix is easy; just add a missing binding to the
substitution we are building up.  It's in the regrettably-subtle
mkGADTVars function.

comment:6 Changed 2 months ago by simonpj

Status: newmerge
Test Case: indexed-types/should_compile/T14162

I believe this fix is also on Richards wip/rae branch.

Worth merging to 8.2 I think, because it's a simple, local change.

comment:7 Changed 2 months ago by simonpj

Milestone: 8.2.2

comment:8 Changed 2 months ago by bgamari

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