From e94c57addafa01a8dfeb7cd17a9e6dabd1d4d85a Mon Sep 17 00:00:00 2001 From: Richard Eisenberg Date: Thu, 10 Dec 2020 23:05:25 -0500 Subject: Unfortunate dirty hack to overcome #18998. See commentary in tcCheckUsage. Close #18998. Test case: typecheck/should_compile/T18998 (cherry picked from commit df7c7faa9998f2b618eab586bb4420d6743aad18) --- compiler/GHC/Tc/Utils/Env.hs | 34 +++++++++++++++++++++- testsuite/tests/typecheck/should_compile/T18998.hs | 14 +++++++++ .../tests/typecheck/should_compile/T18998b.hs | 27 +++++++++++++++++ testsuite/tests/typecheck/should_compile/all.T | 3 ++ 4 files changed, 77 insertions(+), 1 deletion(-) create mode 100644 testsuite/tests/typecheck/should_compile/T18998.hs create mode 100644 testsuite/tests/typecheck/should_compile/T18998b.hs diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs index 76ebb79e1e..25a1de167d 100644 --- a/compiler/GHC/Tc/Utils/Env.hs +++ b/compiler/GHC/Tc/Utils/Env.hs @@ -96,6 +96,7 @@ import GHC.Core.ConLike import GHC.Core.TyCon import GHC.Core.Type import GHC.Core.Coercion.Axiom +import GHC.Core.Coercion import GHC.Core.Class import GHC.Types.Name import GHC.Types.Name.Set @@ -645,10 +646,41 @@ tcCheckUsage name id_mult thing_inside ; wrapper <- case actual_u of Bottom -> return idHsWrapper Zero -> tcSubMult (UsageEnvironmentOf name) Many id_mult - MUsage m -> tcSubMult (UsageEnvironmentOf name) m id_mult + MUsage m -> do { m <- zonkTcType m + ; m <- promote_mult m + ; tcSubMult (UsageEnvironmentOf name) m id_mult } ; tcEmitBindingUsage (deleteUE uenv name) ; return wrapper } + -- This is gross. The problem is in test case typecheck/should_compile/T18998: + -- f :: a %1-> Id n a -> Id n a + -- f x (MkId _) = MkId x + -- where MkId is a GADT constructor. Multiplicity polymorphism of constructors + -- invents a new multiplicity variable p[2] for the application MkId x. This + -- variable is at level 2, bumped because of the GADT pattern-match (MkId _). + -- We eventually unify the variable with One, due to the call to tcSubMult in + -- tcCheckUsage. But by then, we're at TcLevel 1, and so the level-check + -- fails. + -- + -- What to do? If we did inference "for real", the sub-multiplicity constraint + -- would end up in the implication of the GADT pattern-match, and all would + -- be well. But we don't have a real sub-multiplicity constraint to put in + -- the implication. (Multiplicity inference works outside the usual generate- + -- constraints-and-solve scheme.) Here, where the multiplicity arrives, we + -- must promote all multiplicity variables to reflect this outer TcLevel. + -- It's reminiscent of floating a constraint, really, so promotion is + -- appropriate. The promoteTcType function works only on types of kind TYPE rr, + -- so we can't use it here. Thus, this dirtiness. + -- + -- It works nicely in practice. + (promote_mult, _, _, _) = mapTyCo mapper + mapper = TyCoMapper { tcm_tyvar = \ () tv -> do { _ <- promoteTyVar tv + ; zonkTcTyVar tv } + , tcm_covar = \ () cv -> return (mkCoVarCo cv) + , tcm_hole = \ () h -> return (mkHoleCo h) + , tcm_tycobinder = \ () tcv _flag -> return ((), tcv) + , tcm_tycon = return } + {- ********************************************************************* * * The TcBinderStack diff --git a/testsuite/tests/typecheck/should_compile/T18998.hs b/testsuite/tests/typecheck/should_compile/T18998.hs new file mode 100644 index 0000000000..25571bae30 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T18998.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE LinearTypes, GADTs, DataKinds, KindSignatures #-} + +-- this caused a TcLevel assertion failure + +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 a (MkId _) = MkId a diff --git a/testsuite/tests/typecheck/should_compile/T18998b.hs b/testsuite/tests/typecheck/should_compile/T18998b.hs new file mode 100644 index 0000000000..d30a8fdba8 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T18998b.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE ScopedTypeVariables, LinearTypes, DataKinds, TypeOperators, GADTs, + PolyKinds, ConstraintKinds, TypeApplications #-} + +module T18998b where + +import GHC.TypeLits +import Data.Kind +import Unsafe.Coerce + +data Dict :: Constraint -> Type where + Dict :: c => Dict c +knowPred :: Dict (KnownNat (n+1)) -> Dict (KnownNat n) +knowPred Dict = unsafeCoerce (Dict :: Dict ()) +data NList :: Nat -> Type -> Type where + Nil :: NList 0 a + Cons :: a %1-> NList n a %1-> NList (n+1) a +-- Alright, this breaks linearity for some unknown reason + +snoc :: forall n a. KnownNat n => a %1-> NList n a %1-> NList (n+1) a +snoc a Nil = Cons a Nil +snoc a (Cons x (xs :: NList n' a)) = case knowPred (Dict :: Dict (KnownNat n)) of + Dict -> Cons x (snoc a xs) +-- This works fine + +snoc' :: forall n a. a %1-> NList n a %1-> NList (n+1) a +snoc' a Nil = Cons a Nil +snoc' a (Cons x xs) = Cons x (snoc' a xs) diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 0ef2d9ef34..3f9f2cd406 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -720,3 +720,6 @@ test('T17775-viewpats-d', normal, compile_fail, ['']) test('T18118', normal, multimod_compile, ['T18118', '-v0']) test('T18412', normal, compile, ['']) test('T18470', normal, compile, ['']) + +test('T18998', normal, compile, ['']) +test('T18998b', normal, compile, ['']) -- cgit v1.2.1