diff options
author | Richard Eisenberg <rae@richarde.dev> | 2020-12-10 23:05:25 -0500 |
---|---|---|
committer | Ben Gamari <ben@smart-cactus.org> | 2021-01-26 09:49:54 -0500 |
commit | e94c57addafa01a8dfeb7cd17a9e6dabd1d4d85a (patch) | |
tree | 646fcb0042e8505dd1a055bc0ca34f854bb41d80 | |
parent | 679a858723bf653d86625535dbd7542aeea64559 (diff) | |
download | haskell-e94c57addafa01a8dfeb7cd17a9e6dabd1d4d85a.tar.gz |
Unfortunate dirty hack to overcome #18998.
See commentary in tcCheckUsage.
Close #18998.
Test case: typecheck/should_compile/T18998
(cherry picked from commit df7c7faa9998f2b618eab586bb4420d6743aad18)
-rw-r--r-- | compiler/GHC/Tc/Utils/Env.hs | 34 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/T18998.hs | 14 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/T18998b.hs | 27 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 3 |
4 files changed, 77 insertions, 1 deletions
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, ['']) |