Commit ac704fca authored by simonpj@microsoft.com's avatar simonpj@microsoft.com

Add assertion checks for mkCoVar/mkTyVar

A type variable has a flag saying whether it is a *type* variable or
a *coercion* variable.  This patch adds assertions to check the flag.

And it adds fixes to places which were Wrong (and hence fired the
assertion)! 

Also removed isCoVar from Coercion, since it's done by Var.isCoVar.

parent 28d732c3
......@@ -40,6 +40,10 @@ import {-# SOURCE #-} TypeRep( Type, Kind )
import {-# SOURCE #-} TcType( TcTyVarDetails, pprTcTyVarDetails )
import {-# SOURCE #-} IdInfo( GlobalIdDetails, notGlobalId,
IdInfo, seqIdInfo )
#ifdef DEBUG
import {-# SOURCE #-} TypeRep( isCoercionKind )
#endif
import Name hiding (varName)
import Unique
import FastTypes
......@@ -187,7 +191,8 @@ setTyVarKind tv k = tv {tyVarKind = k}
\begin{code}
mkTyVar :: Name -> Kind -> TyVar
mkTyVar name kind = TyVar { varName = name
mkTyVar name kind = ASSERT( not (isCoercionKind kind ) )
TyVar { varName = name
, realUnique = getKey# (nameUnique name)
, tyVarKind = kind
, isCoercionVar = False
......@@ -195,22 +200,12 @@ mkTyVar name kind = TyVar { varName = name
mkTcTyVar :: Name -> Kind -> TcTyVarDetails -> TyVar
mkTcTyVar name kind details
= TcTyVar { varName = name,
= ASSERT( not (isCoercionKind kind) )
TcTyVar { varName = name,
realUnique = getKey# (nameUnique name),
tyVarKind = kind,
tcTyVarDetails = details
}
mkWildCoVar :: Kind -> TyVar
-- A type variable that is never referred to,
-- so its unique doesn't matter
mkWildCoVar kind
= TyVar { varName = mkSysTvName wild_uniq FSLIT("co_wild"),
realUnique = _ILIT(1),
tyVarKind = kind,
isCoercionVar = True }
where
wild_uniq = mkBuiltinUnique 1
\end{code}
%************************************************************************
......@@ -228,12 +223,24 @@ setCoVarUnique = setVarUnique
setCoVarName = setVarName
mkCoVar :: Name -> Kind -> CoVar
mkCoVar name kind = TyVar { varName = name
mkCoVar name kind = ASSERT( isCoercionKind kind )
TyVar { varName = name
, realUnique = getKey# (nameUnique name)
, tyVarKind = kind
, isCoercionVar = True
}
mkWildCoVar :: Kind -> TyVar
-- A type variable that is never referred to,
-- so its unique doesn't matter
mkWildCoVar kind
= ASSERT( isCoercionKind kind )
TyVar { varName = mkSysTvName wild_uniq FSLIT("co_wild"),
realUnique = _ILIT(1),
tyVarKind = kind,
isCoercionVar = True }
where
wild_uniq = mkBuiltinUnique 1
\end{code}
%************************************************************************
......
......@@ -1120,7 +1120,8 @@ eta_expand n us expr ty
Lam lam_tv (eta_expand n us2 (App expr (Type (mkTyVarTy lam_tv))) (substTyWith [tv] [mkTyVarTy lam_tv] ty'))
where
lam_tv = mkTyVar (mkSysTvName uniq FSLIT("etaT")) (tyVarKind tv)
lam_tv = setVarName tv (mkSysTvName uniq FSLIT("etaT"))
-- Using tv as a base retains its tyvar/covar-ness
(uniq:us2) = us
; Nothing ->
......
......@@ -1010,8 +1010,11 @@ bindIfaceTyVars bndrs thing_inside
(occs,kinds) = unzip bndrs
mk_iface_tyvar :: Name -> IfaceKind -> IfL TyVar
mk_iface_tyvar name ifKind = do { kind <- tcIfaceType ifKind
; return (Var.mkTyVar name kind)
}
mk_iface_tyvar name ifKind
= do { kind <- tcIfaceType ifKind
; if isCoercionKind kind then
return (Var.mkCoVar name kind)
else
return (Var.mkTyVar name kind) }
\end{code}
......@@ -44,7 +44,6 @@ import Id ( Id, idType, isDataConWorkId, idOccInfo, isDictId,
)
import NewDemand ( isStrictDmd, isBotRes, splitStrictSig )
import SimplMonad
import Var ( tyVarKind, mkTyVar )
import Name ( mkSysTvName )
import Type ( Type, splitFunTys, dropForAlls, isStrictType,
splitTyConApp_maybe, tyConAppArgs, mkTyVarTys )
......
......@@ -94,7 +94,7 @@ instToVar (LitInst {tci_name = nm, tci_ty = ty})
instToVar (Method {tci_id = id})
= id
instToVar (Dict {tci_name = nm, tci_pred = pred})
| isEqPred pred = Var.mkTyVar nm (mkPredTy pred)
| isEqPred pred = Var.mkCoVar nm (mkPredTy pred)
| otherwise = mkLocalId nm (mkPredTy pred)
instLoc inst = tci_loc inst
......
......@@ -39,7 +39,7 @@ module Coercion (
import TypeRep
import Type
import TyCon
import Var hiding (isCoVar)
import Var
import Name
import OccName
import PrelNames
......@@ -91,9 +91,6 @@ splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe c
splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
splitCoercionKind_maybe other = Nothing
isCoVar :: Var -> Bool
isCoVar tv = isTyVar tv && isCoercionKind (tyVarKind tv)
type Coercion = Type
type CoercionKind = Kind -- A CoercionKind is always of form (ty1 :=: ty2)
......
......@@ -1289,7 +1289,7 @@ substTyVarBndr subst@(TvSubst in_scope env) old_var
| is_co_var = setTyVarKind old_var (substTy subst kind)
| otherwise = old_var
kind = tyVarKind old_var
is_co_var = isCoercionKind kind
is_co_var = isCoVar old_var
\end{code}
----------------------------------------------------
......@@ -1465,14 +1465,6 @@ defaultKind k
| isSubArgTypeKind k = liftedTypeKind
| otherwise = k
isCoercionKind :: Kind -> Bool
-- All coercions are of form (ty1 :=: ty2)
-- This function is here rather than in Coercion,
-- because it's used by substTy
isCoercionKind k | Just k' <- kindView k = isCoercionKind k'
isCoercionKind (PredTy (EqPred {})) = True
isCoercionKind other = False
isEqPred :: PredType -> Bool
isEqPred (EqPred _ _) = True
isEqPred other = False
......
......@@ -22,7 +22,7 @@ module TypeRep (
liftedTypeKind, unliftedTypeKind, openTypeKind,
argTypeKind, ubxTupleKind,
isLiftedTypeKindCon, isLiftedTypeKind,
mkArrowKind, mkArrowKinds,
mkArrowKind, mkArrowKinds, isCoercionKind,
-- Kind constructors...
liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
......@@ -386,14 +386,21 @@ isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
isCoSuperKind other = False
-------------------
-- lastly we need a few functions on Kinds
-- Lastly we need a few functions on Kinds
isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey
isLiftedTypeKind :: Kind -> Bool
isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
isLiftedTypeKind other = False
isCoercionKind :: Kind -> Bool
-- All coercions are of form (ty1 :=: ty2)
-- This function is here rather than in Coercion,
-- because it's used in a knot-tied way to enforce invariants in Var
isCoercionKind (NoteTy _ k) = isCoercionKind k
isCoercionKind (PredTy (EqPred {})) = True
isCoercionKind other = False
\end{code}
......
......@@ -12,6 +12,8 @@ type SuperKind = Type
tySuperKind :: SuperKind
coSuperKind :: SuperKind
isCoercionKind :: Kind -> Bool
isCoSuperKind :: SuperKind -> Bool
\end{code}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment