Linear types: level numbers assertion failure
The following program causes an assertion failure in HEAD, a violation in checkTcLevelInvariant
.
{-# LANGUAGE LinearTypes, GADTs, DataKinds, KindSignatures #-}
module T18998 where
import GHC.Types
import GHC.TypeLits
data Id :: Nat -> Type -> Type where
MkId :: a %1-> Id 0 a
f :: a %1-> Id n a -> Id n a
f x (MkId _) = MkId x
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 9.1.0.20201124:
ASSERT failed!
(t_aAj{tv} Nothing [tau:2] :: GHC.Types.Multiplicity{(w) tc 36c})
2
1
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Utils/Panic.hs:300:5 in ghc:GHC.Utils.Panic
assertPprPanic, called at compiler/GHC/Tc/Utils/TcType.hs:973:76 in ghc:GHC.Tc.Utils.TcType
Credits to Divesh Otwani for finding the intial version of this bug.