[Git][ghc/ghc][master] Unfortunate dirty hack to overcome #18998.
Marge Bot
gitlab at gitlab.haskell.org
Thu Dec 17 18:57:57 UTC 2020
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
df7c7faa by Richard Eisenberg at 2020-12-17T13:57:48-05:00
Unfortunate dirty hack to overcome #18998.
See commentary in tcCheckUsage.
Close #18998.
Test case: typecheck/should_compile/T18998
- - - - -
4 changed files:
- compiler/GHC/Tc/Utils/Env.hs
- + testsuite/tests/typecheck/should_compile/T18998.hs
- + testsuite/tests/typecheck/should_compile/T18998b.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Tc/Utils/Env.hs
=====================================
@@ -102,6 +102,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.Unit.Module
@@ -663,10 +664,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
=====================================
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
=====================================
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)
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -749,3 +749,6 @@ test('TyAppPat_UniversalMulti2', normal, compile, [''])
test('TyAppPat_UniversalMulti3', normal, compile, [''])
test('TyAppPat_UniversalNested', normal, compile, [''])
test('TyAppPat_Wildcard', normal, compile, [''])
+
+test('T18998', normal, compile, [''])
+test('T18998b', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/df7c7faa9998f2b618eab586bb4420d6743aad18
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/df7c7faa9998f2b618eab586bb4420d6743aad18
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20201217/1f6bf00e/attachment-0001.html>
More information about the ghc-commits
mailing list