diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2018-10-16 12:38:16 +0100 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2018-10-24 16:38:55 +0100 |
commit | 0faf7fd3e6c652575af9993787f07cad86f452f6 (patch) | |
tree | 029d5a626ac2677305151120cd4a0a4a144c6493 /compiler/basicTypes/Id.hs | |
parent | 321bc1a644a9e4598a4af30d4aeae315f0ff487a (diff) | |
download | haskell-0faf7fd3e6c652575af9993787f07cad86f452f6.tar.gz |
Refactor the treatment of predicate types
Trac #15648 showed that GHC was a bit confused about the
difference between the types for
* Predicates
* Coercions
* Evidence (in the typechecker constraint solver)
This patch cleans it up. See especially Type.hs
Note [Types for coercions, predicates, and evidence]
Particular changes
* Coercion types (a ~# b) and (a ~#R b) are not predicate types
(so isPredTy reports False for them) and are not implicitly
instantiated by the type checker. This is a real change, but
it consistently reflects that fact that (~#) and (~R#) really
are different from predicates.
* isCoercionType is renamed to isCoVarType
* During type inference, simplifyInfer, we do /not/ want to infer
a constraint (a ~# b), because that is no longer a predicate type.
So we 'lift' it to (a ~ b). See TcType
Note [Lift equality constaints when quantifying]
* During type inference for pattern synonyms, we need to 'lift'
provided constraints of type (a ~# b) to (a ~ b). See
Note [Equality evidence in pattern synonyms] in PatSyn
* But what about (forall a. Eq a => a ~# b)? Is that a
predicate type? No -- it does not have kind Constraint.
Is it an evidence type? Perhaps, but awkwardly so.
In the end I decided NOT to make it an evidence type,
and to ensure the the type inference engine never
meets it. This made me /simplify/ the code in
TcCanonical.makeSuperClasses; see TcCanonical
Note [Equality superclasses in quantified constraints]
Instead I moved the special treatment for primitive
equality to TcInteract.doTopReactOther. See TcInteract
Note [Looking up primitive equalities in quantified constraints]
Also see Note [Evidence for quantified constraints] in Type.
All this means I can have
isEvVarType ty = isCoVarType ty || isPredTy ty
which is nice.
All in all, rather a lot of work for a small refactoring,
but I think it's a real improvement.
Diffstat (limited to 'compiler/basicTypes/Id.hs')
-rw-r--r-- | compiler/basicTypes/Id.hs | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/compiler/basicTypes/Id.hs b/compiler/basicTypes/Id.hs index c1d281edd6..78518ee094 100644 --- a/compiler/basicTypes/Id.hs +++ b/compiler/basicTypes/Id.hs @@ -267,20 +267,20 @@ mkVanillaGlobalWithInfo = mkGlobalId VanillaId -- | For an explanation of global vs. local 'Id's, see "Var#globalvslocal" mkLocalId :: Name -> Type -> Id mkLocalId name ty = mkLocalIdWithInfo name ty vanillaIdInfo - -- It's tempting to ASSERT( not (isCoercionType ty) ), but don't. Sometimes, + -- It's tempting to ASSERT( not (isCoVarType ty) ), but don't. Sometimes, -- the type is a panic. (Search invented_id) -- | Make a local CoVar mkLocalCoVar :: Name -> Type -> CoVar mkLocalCoVar name ty - = ASSERT( isCoercionType ty ) + = ASSERT( isCoVarType ty ) Var.mkLocalVar CoVarId name ty vanillaIdInfo -- | Like 'mkLocalId', but checks the type to see if it should make a covar mkLocalIdOrCoVar :: Name -> Type -> Id mkLocalIdOrCoVar name ty - | isCoercionType ty = mkLocalCoVar name ty - | otherwise = mkLocalId name ty + | isCoVarType ty = mkLocalCoVar name ty + | otherwise = mkLocalId name ty -- | Make a local id, with the IdDetails set to CoVarId if the type indicates -- so. @@ -288,8 +288,8 @@ mkLocalIdOrCoVarWithInfo :: Name -> Type -> IdInfo -> Id mkLocalIdOrCoVarWithInfo name ty info = Var.mkLocalVar details name ty info where - details | isCoercionType ty = CoVarId - | otherwise = VanillaId + details | isCoVarType ty = CoVarId + | otherwise = VanillaId -- proper ids only; no covars! mkLocalIdWithInfo :: Name -> Type -> IdInfo -> Id @@ -311,7 +311,7 @@ mkExportedVanillaId name ty = Var.mkExportedLocalVar VanillaId name ty vanillaId -- | Create a system local 'Id'. These are local 'Id's (see "Var#globalvslocal") -- that are created by the compiler out of thin air mkSysLocal :: FastString -> Unique -> Type -> Id -mkSysLocal fs uniq ty = ASSERT( not (isCoercionType ty) ) +mkSysLocal fs uniq ty = ASSERT( not (isCoVarType ty) ) mkLocalId (mkSystemVarName uniq fs) ty -- | Like 'mkSysLocal', but checks to see if we have a covar type @@ -328,7 +328,7 @@ mkSysLocalOrCoVarM fs ty -- | Create a user local 'Id'. These are local 'Id's (see "Var#globalvslocal") with a name and location that the user might recognize mkUserLocal :: OccName -> Unique -> Type -> SrcSpan -> Id -mkUserLocal occ uniq ty loc = ASSERT( not (isCoercionType ty) ) +mkUserLocal occ uniq ty loc = ASSERT( not (isCoVarType ty) ) mkLocalId (mkInternalName uniq occ loc) ty -- | Like 'mkUserLocal', but checks if we have a coercion type @@ -585,7 +585,7 @@ isDeadBinder bndr | isId bndr = isDeadOcc (idOccInfo bndr) -} isEvVar :: Var -> Bool -isEvVar var = isPredTy (varType var) +isEvVar var = isEvVarType (varType var) isDictId :: Id -> Bool isDictId id = isDictTy (idType id) |