diff options
| -rw-r--r-- | compiler/coreSyn/CoreLint.hs | 2 | ||||
| -rw-r--r-- | compiler/coreSyn/CoreSyn.hs | 21 | ||||
| -rw-r--r-- | compiler/typecheck/TcType.hs | 2 | ||||
| -rw-r--r-- | compiler/types/Kind.hs | 10 |
4 files changed, 25 insertions, 10 deletions
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs index 50c1ac13de..8f47d5e404 100644 --- a/compiler/coreSyn/CoreLint.hs +++ b/compiler/coreSyn/CoreLint.hs @@ -1030,7 +1030,7 @@ lintAndScopeId id linterF (text "Non-local Id binder" <+> ppr id) -- See Note [Checking for global Ids] ; (ty, k) <- lintInTy (idType id) - ; lintL (not (isRuntimeRepPolymorphic k)) + ; lintL (not (isLevityPolymorphic k)) (text "RuntimeRep-polymorphic binder:" <+> (ppr id <+> dcolon <+> parens (ppr ty <+> dcolon <+> ppr k))) ; let id' = setIdType id ty diff --git a/compiler/coreSyn/CoreSyn.hs b/compiler/coreSyn/CoreSyn.hs index 01a864b4ea..cb84e27b5b 100644 --- a/compiler/coreSyn/CoreSyn.hs +++ b/compiler/coreSyn/CoreSyn.hs @@ -169,10 +169,11 @@ These data types are the heart of the compiler -- * Primitive literals -- -- * Applications: note that the argument may be a 'Type'. --- --- See "CoreSyn#let_app_invariant" for another invariant +-- See Note [CoreSyn let/app invariant] +-- See Note [Levity polymorphism invariants] -- -- * Lambda abstraction +-- See Note [Levity polymorphism invariants] -- -- * Recursive and non recursive @let@s. Operationally -- this corresponds to allocating a thunk for the things @@ -186,6 +187,7 @@ These data types are the heart of the compiler -- the meaning of /lifted/ vs. /unlifted/). -- -- See Note [CoreSyn let/app invariant] +-- See Note [Levity polymorphism invariants] -- -- #type_let# -- We allow a /non-recursive/ let to bind a type variable, thus: @@ -199,7 +201,7 @@ These data types are the heart of the compiler -- in a Let expression, rather than at top level. We may want to revist -- this choice. -- --- * Case split. Operationally this corresponds to evaluating +-- * Case expression. Operationally this corresponds to evaluating -- the scrutinee (expression examined) to weak head normal form -- and then examining at most one level of resulting constructor (i.e. you -- cannot do nested pattern matching directly with this). @@ -381,6 +383,19 @@ Note [CoreSyn case invariants] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ See #case_invariants# +Note [Levity polymorphism invariants] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The levity-polymorphism invariants are these: + +* The type of a term-binder must not be levity-polymorphic +* The type of the argument of an App must not be levity-polymorphic. + +A type (t::TYPE r) is "levity polymorphic" if 'r' has any free variables. + +For example + (\(r::RuntimeRep). \(a::TYPE r). \(x::a). e +is illegal because x's type has kind (TYPE r), which has 'r' free. + Note [CoreSyn let goal] ~~~~~~~~~~~~~~~~~~~~~~~ * The simplifier tries to ensure that if the RHS of a let is a constructor diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 099502d9a3..d31ed3a48e 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -142,7 +142,7 @@ module TcType ( mkClassPred, isDictLikeTy, tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy, - isRuntimeRepVar, isRuntimeRepPolymorphic, + isRuntimeRepVar, isLevityPolymorphic, isVisibleBinder, isInvisibleBinder, -- Type substitutions diff --git a/compiler/types/Kind.hs b/compiler/types/Kind.hs index c31169e03d..4db98fc25c 100644 --- a/compiler/types/Kind.hs +++ b/compiler/types/Kind.hs @@ -14,7 +14,7 @@ module Kind ( classifiesTypeWithValues, isStarKind, isStarKindSynonymTyCon, - isRuntimeRepPolymorphic + isLevityPolymorphic ) where #include "HsVersions.h" @@ -77,10 +77,10 @@ returnsTyCon _ _ = False returnsConstraintKind :: Kind -> Bool returnsConstraintKind = returnsTyCon constraintKindTyConKey --- | Tests whether the given type (which should look like "TYPE ...") has any --- free variables -isRuntimeRepPolymorphic :: Kind -> Bool -isRuntimeRepPolymorphic k +-- | Tests whether the given kind (which should look like "TYPE ...") +-- has any free variables +isLevityPolymorphic :: Kind -> Bool +isLevityPolymorphic k = not $ isEmptyVarSet $ tyCoVarsOfType k -------------------------------------------- |