Commit ff818166 authored by simonpj's avatar simonpj
Browse files

[project @ 2005-03-01 21:40:40 by simonpj]

Type signatures and skolem constants (again)
		Merge to STABLE

This commit lays to rest the vexed question of skolem constants
and type signatures.  My fix last week made type-signature variables
into ordinary meta type variables, because they can be unified
together (see Note [Signature skolems] in TcType).  But that was wrong
becuase GADTs will only refine skolems.

So this commit extends TcTyVarDetails with a new constructors, SigSkolTv,
which is a skolem (like SkolemTv) but is unifiable (like MetaTv).  It's
a bit of a hack, but the code came out quite nicely.

Now the GADT tests work.
parent 70768203
......@@ -39,7 +39,7 @@ import TcMType ( newTyFlexiVarTy, zonkQuantifiedTyVar,
import TcType ( TcTyVar, SkolemInfo(SigSkol),
TcTauType, TcSigmaType,
mkTyVarTy, mkForAllTys, mkFunTys, tyVarsOfType,
mkForAllTy, isUnLiftedType, tcGetTyVar_maybe,
mkForAllTy, isUnLiftedType, tcGetTyVar,
mkTyVarTys, tidyOpenTyVar, tidyOpenType )
import Kind ( argTypeKind )
import VarEnv ( TyVarEnv, emptyVarEnv, lookupVarEnv, extendVarEnv, emptyTidyEnv )
......@@ -561,26 +561,7 @@ getMonoBindInfo tc_binds
%* *
%************************************************************************
Type signatures are tricky. Consider
x :: [a]
y :: b
(x,y,z) = ([y,z], z, head x)
Here, x and y have type sigs, which go into the environment. We used to
instantiate their types with skolem constants, and push those types into
the RHS, so we'd typecheck the RHS with type
( [a*], b*, c )
where a*, b* are skolem constants, and c is an ordinary meta type varible.
The trouble is that the occurrences of z in the RHS force a* and b* to
be the *same*, so we can't make them into skolem constants that don't unify
with each other. Alas.
Current solution: don't use skolems at all. Instead, instantiate the type
signatures with ordinary meta type variables, and check at the end that
each group has remained distinct.
Type signatures are tricky. See Note [Signature skolems] in TcType
\begin{code}
tcTySigs :: [LSig Name] -> TcM [TcSigInfo]
......@@ -612,8 +593,10 @@ tcTySig :: LSig Name -> TcM TcSigInfo
tcTySig (L span (Sig (L _ name) ty))
= setSrcSpan span $
do { sigma_ty <- tcHsSigType (FunSigCtxt name) ty
; let rigid_info = SigSkol name
poly_id = mkLocalId name sigma_ty
; (tvs, theta, tau) <- tcInstSigType name sigma_ty
; loc <- getInstLoc (SigOrigin (SigSkol name))
; let poly_id = mkLocalId name sigma_ty
-- The scoped names are the ones explicitly mentioned
-- in the HsForAll. (There may be more in sigma_ty, because
......@@ -622,8 +605,6 @@ tcTySig (L span (Sig (L _ name) ty))
L _ (HsForAllTy _ tvs _ _) -> hsLTyVarNames tvs
other -> []
; (tvs, theta, tau) <- tcInstSigType sigma_ty
; loc <- getInstLoc (SigOrigin rigid_info)
; return (TcSigInfo { sig_id = poly_id, sig_scoped = scoped_names,
sig_tvs = tvs, sig_theta = theta, sig_tau = tau,
sig_loc = loc }) }
......@@ -721,26 +702,26 @@ checkDistinctTyVars sig_tvs
; return zonked_tvs }
where
zonk_one sig_tv = do { ty <- zonkTcTyVar sig_tv
; case tcGetTyVar_maybe ty of
Just tv' -> return tv'
Nothing -> bomb_out sig_tv "a type" ty }
; return (tcGetTyVar "checkDistinctTyVars" ty) }
-- 'ty' is bound to be a type variable, because SigSkolTvs
-- can only be unified with type variables
check_dup :: TyVarEnv TcTyVar -> (TcTyVar, TcTyVar) -> TcM (TyVarEnv TcTyVar)
-- The TyVarEnv maps each zonked type variable back to its
-- corresponding user-written signature type variable
check_dup acc (sig_tv, zonked_tv)
= case lookupVarEnv acc zonked_tv of
Just sig_tv' -> bomb_out sig_tv "another quantified type variable"
(mkTyVarTy sig_tv')
Just sig_tv' -> bomb_out sig_tv sig_tv'
Nothing -> return (extendVarEnv acc zonked_tv sig_tv)
bomb_out sig_tv doc ty
= failWithTc (ptext SLIT("Quantified type variable") <+> quotes (ppr tidy_tv)
<+> ptext SLIT("is unified with") <+> text doc <+> ppr tidy_ty)
bomb_out sig_tv1 sig_tv2
= failWithTc (ptext SLIT("Quantified type variable") <+> quotes (ppr tidy_tv1)
<+> ptext SLIT("is unified with another quantified type variable")
<+> ppr tidy_tv2)
where
(env1, tidy_tv) = tidyOpenTyVar emptyTidyEnv sig_tv
(_env2, tidy_ty) = tidyOpenType env1 ty
(env1, tidy_tv1) = tidyOpenTyVar emptyTidyEnv sig_tv1
(_env2, tidy_tv2) = tidyOpenTyVar env1 sig_tv2
\end{code}
......
......@@ -29,7 +29,7 @@ module TcMType (
Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
checkValidInstHead, instTypeErr, checkAmbiguity,
arityErr, isRigidType,
arityErr,
--------------------------------
-- Zonking
......@@ -122,22 +122,6 @@ newTyFlexiVarTy kind
newTyFlexiVarTys :: Int -> Kind -> TcM [TcType]
newTyFlexiVarTys n kind = mappM newTyFlexiVarTy (nOfThem n kind)
isRigidType :: TcType -> TcM Bool
-- Check that the type is rigid, *taking the type refinement into account*
-- In other words if a rigid type variable tv is refined to a wobbly type,
-- the answer should be False
-- ToDo: can this happen?
isRigidType ty
= do { rigids <- mapM is_rigid (varSetElems (tyVarsOfType ty))
; return (and rigids) }
where
is_rigid tv = do { details <- lookupTcTyVar tv
; case details of
RigidTv -> return True
IndirectTv True ty -> isRigidType ty
other -> return False
}
newKindVar :: TcM TcKind
newKindVar = do { uniq <- newUnique
; ref <- newMutVar Nothing
......@@ -177,11 +161,9 @@ tcInstTyVars tyvars
-- they cannot possibly be captured by
-- any existing for-alls. Hence zipTopTvSubst
tcInstTyVar tyvar -- Use the OccName of the tyvar we are instantiating
-- but make a System Name, so that it's updated in
-- preference to a tcInstSigTyVar
tcInstTyVar tyvar -- Freshen the Name of the tyvar
= do { uniq <- newUnique
; newMetaTyVar (mkSystemName uniq (getOccName tyvar))
; newMetaTyVar (setNameUnique (tyVarName tyvar) uniq)
(tyVarKind tyvar) Flexi }
tcInstType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
......@@ -192,25 +174,24 @@ tcInstType ty = tc_inst_type (mappM tcInstTyVar) ty
---------------------------------------------
tcInstSigType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
-- Instantiate a type with fresh meta type variables, but
-- ones which have the same Name as the original type
-- variable. This is used for type signatures, where we must
-- instantiate with meta type variables, but we'd like to avoid
-- instantiating them were possible; and the unifier unifies
-- tyvars with System Names by preference
tcInstSigType :: Name -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
-- Instantiate a type with fresh SigSkol variables
-- See Note [Signature skolems] in TcType.
--
-- Tne new type variables have the sane Name as the original.
-- We don't need a fresh unique, because the renamer has made them
-- unique, and it's better not to do so because we extend the envt
-- with them as scoped type variables, and we'd like to avoid spurious
-- 's = s' bindings in error messages
tcInstSigType ty = tc_inst_type tcInstSigTyVars ty
tcInstSigType id_name ty = tc_inst_type (tcInstSigTyVars id_name) ty
tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
tcInstSigTyVars tyvars
tcInstSigTyVars :: Name -> [TyVar] -> TcM [TcTyVar]
tcInstSigTyVars id_name tyvars
= mapM new_tv tyvars
where
new_tv tv = newMetaTyVar (tyVarName tv) (tyVarKind tv) Flexi
new_tv tv = do { ref <- newMutVar Flexi ;
; return (mkTcTyVar (tyVarName tv) (tyVarKind tv)
(SigSkolTv id_name ref)) }
---------------------------------------------
......@@ -299,8 +280,7 @@ We return Nothing iff the original box was unbound.
\begin{code}
data LookupTyVarResult -- The result of a lookupTcTyVar call
= FlexiTv
| RigidTv
= DoneTv TcTyVarDetails
| IndirectTv Bool TcType
-- True => This is a non-wobbly type refinement,
-- gotten from GADT match unification
......@@ -311,31 +291,47 @@ lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
-- This function is the ONLY PLACE that we consult the
-- type refinement carried by the monad
lookupTcTyVar tyvar
= case tcTyVarDetails tyvar of
= let
details = tcTyVarDetails tyvar
in
case details of
MetaTv ref -> lookup_wobbly details ref
SkolemTv _ -> do { type_reft <- getTypeRefinement
; case lookupVarEnv type_reft tyvar of
Just ty -> return (IndirectTv True ty)
Nothing -> return RigidTv
}
MetaTv ref -> do { details <- readMutVar ref
; case details of
Indirect ty -> return (IndirectTv False ty)
Flexi -> return FlexiTv
Nothing -> return (DoneTv details)
}
-- For SigSkolTvs try the refinement, and, failing that
-- see if it's been unified to anything. It's a combination
-- of SkolemTv and MetaTv
SigSkolTv _ ref -> do { type_reft <- getTypeRefinement
; case lookupVarEnv type_reft tyvar of
Just ty -> return (IndirectTv True ty)
Nothing -> lookup_wobbly details ref
}
-- Look up a meta type variable, conditionally consulting
-- the current type refinement
condLookupTcTyVar :: Bool -> TcTyVar -> TcM LookupTyVarResult
condLookupTcTyVar use_refinement tyvar
| use_refinement = lookupTcTyVar tyvar
| otherwise
= case tcTyVarDetails tyvar of
SkolemTv _ -> return RigidTv
MetaTv ref -> do { details <- readMutVar ref
; case details of
Indirect ty -> return (IndirectTv False ty)
Flexi -> return FlexiTv
}
= case details of
MetaTv ref -> lookup_wobbly details ref
SkolemTv _ -> return (DoneTv details)
SigSkolTv _ ref -> lookup_wobbly details ref
where
details = tcTyVarDetails tyvar
lookup_wobbly :: TcTyVarDetails -> IORef MetaDetails -> TcM LookupTyVarResult
lookup_wobbly details ref
= do { meta_details <- readMutVar ref
; case meta_details of
Indirect ty -> return (IndirectTv False ty)
Flexi -> return (DoneTv details)
}
{-
-- gaw 2004 We aren't shorting anything out anymore, at least for now
......@@ -563,9 +559,9 @@ zonkTyVar unbound_var_fn rflag tyvar
-- If b is true, the variable was refined, and therefore it is okay
-- to continue refining inside. Otherwise it was wobbly and we should
-- not refine further inside.
IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
FlexiTv -> unbound_var_fn tyvar -- Unbound flexi
RigidTv -> return (TyVarTy tyvar) -- Rigid, no zonking necessary
IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
DoneTv (MetaTv _) -> unbound_var_fn tyvar -- Unbound meta type variable
DoneTv other -> return (TyVarTy tyvar) -- Rigid, no zonking necessary
\end{code}
......
......@@ -25,7 +25,7 @@ import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2,
tcLookupClass, tcLookupDataCon, tcLookupId )
import TcMType ( newTyFlexiVarTy, arityErr, tcSkolTyVars, readMetaTyVar )
import TcType ( TcType, TcTyVar, TcSigmaType, TcTauType, zipTopTvSubst,
SkolemInfo(PatSkol), isSkolemTyVar, isMetaTyVar, pprSkolemTyVar,
SkolemInfo(PatSkol), isSkolemTyVar, isMetaTyVar, pprTcTyVar,
TvSubst, mkOpenTvSubst, substTyVar, substTy, MetaDetails(..),
mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy )
import VarEnv ( mkVarEnv ) -- ugly
......@@ -634,9 +634,7 @@ badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
lazyPatErr pat tvs
= failWithTc $
hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))
2 (vcat (map get tvs))
where
get tv = ASSERT( isSkolemTyVar tv ) pprSkolemTyVar tv
2 (vcat (map pprTcTyVar tvs))
inaccessibleAlt msg
= hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
......
......@@ -50,7 +50,7 @@ import HscTypes ( FixityEnv,
import Packages ( PackageId )
import Type ( Type, TvSubstEnv, pprParendType, pprTyThingCategory )
import TcType ( TcTyVarSet, TcType, TcTauType, TcThetaType, SkolemInfo,
TcPredType, TcKind, tcCmpPred, tcCmpType, tcCmpTypes )
TcPredType, TcKind, tcCmpPred, tcCmpType, tcCmpTypes, pprSkolInfo )
import InstEnv ( DFunId, InstEnv )
import IOEnv
import RdrName ( GlobalRdrEnv, LocalRdrEnv )
......@@ -779,8 +779,6 @@ data InstOrigin
\begin{code}
pprInstLoc :: InstLoc -> SDoc
pprInstLoc (InstLoc (SigOrigin info) locn _)
= text "arising from" <+> ppr info -- I don't think this happens much, if at all
pprInstLoc (InstLoc orig locn _)
= hsep [text "arising from", pp_orig orig, text "at", ppr locn]
where
......@@ -791,11 +789,11 @@ pprInstLoc (InstLoc orig locn _)
pp_orig (LiteralOrigin lit) = hsep [ptext SLIT("the literal"), quotes (ppr lit)]
pp_orig (ArithSeqOrigin seq) = hsep [ptext SLIT("the arithmetic sequence"), quotes (ppr seq)]
pp_orig (PArrSeqOrigin seq) = hsep [ptext SLIT("the parallel array sequence"), quotes (ppr seq)]
pp_orig InstSigOrigin = ptext SLIT("instantiating a type signature")
pp_orig InstScOrigin = ptext SLIT("the superclasses of an instance declaration")
pp_orig InstSigOrigin = ptext SLIT("instantiating a type signature")
pp_orig InstScOrigin = ptext SLIT("the superclasses of an instance declaration")
pp_orig DerivOrigin = ptext SLIT("the 'deriving' clause of a data type declaration")
pp_orig DefaultOrigin = ptext SLIT("a 'default' declaration")
pp_orig DoOrigin = ptext SLIT("a do statement")
pp_orig ProcOrigin = ptext SLIT("a proc expression")
pp_orig (SigOrigin info) = ppr info
pp_orig DoOrigin = ptext SLIT("a do statement")
pp_orig ProcOrigin = ptext SLIT("a proc expression")
pp_orig (SigOrigin info) = pprSkolInfo info
\end{code}
......@@ -23,9 +23,9 @@ module TcType (
--------------------------------
-- MetaDetails
Expected(..), TcRef, TcTyVarDetails(..),
MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolemTyVar,
isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, skolemTvInfo, metaTvRef,
isFlexi, isIndirect,
MetaDetails(Flexi, Indirect), SkolemInfo(..), pprTcTyVar, pprSkolInfo,
isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, metaTvRef,
isFlexi, isIndirect,
--------------------------------
-- Builders
......@@ -247,13 +247,45 @@ checking. It's attached to mutable type variables only.
It's knot-tied back to Var.lhs. There is no reason in principle
why Var.lhs shouldn't actually have the definition, but it "belongs" here.
Note [Signature skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
Consider this
x :: [a]
y :: b
(x,y,z) = ([y,z], z, head x)
Here, x and y have type sigs, which go into the environment. We used to
instantiate their types with skolem constants, and push those types into
the RHS, so we'd typecheck the RHS with type
( [a*], b*, c )
where a*, b* are skolem constants, and c is an ordinary meta type varible.
The trouble is that the occurrences of z in the RHS force a* and b* to
be the *same*, so we can't make them into skolem constants that don't unify
with each other. Alas.
On the other hand, we *must* use skolems for signature type variables,
becuase GADT type refinement refines skolems only.
One solution woudl be insist that in the above defn the programmer uses
the same type variable in both type signatures. But that takes explanation.
The alternative (currently implemented) is to have a special kind of skolem
constant, SigSkokTv, which can unify with other SigSkolTvs.
\begin{code}
type TcTyVar = TyVar -- Used only during type inference
-- A TyVarDetails is inside a TyVar
data TcTyVarDetails
= SkolemTv SkolemInfo -- A skolem constant
| MetaTv (IORef MetaDetails) -- A meta type variable stands for a tau-type
= MetaTv (IORef MetaDetails) -- A meta type variable stands for a tau-type
| SkolemTv SkolemInfo -- A skolem constant
| SigSkolTv Name (IORef MetaDetails) -- Ditto, but from a type signature;
-- see Note [Signature skolems]
-- The MetaDetails, if filled in, will
-- always be another SigSkolTv
data SkolemInfo
= SigSkol Name -- Bound at a type signature
......@@ -282,30 +314,34 @@ tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
-- Tidy the type inside a GenSkol, preparatory to printing it
tidySkolemTyVar env tv
= ASSERT( isSkolemTyVar tv )
(env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv info1))
(env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
where
(env1, info1) = case skolemTvInfo tv of
GenSkol tvs ty loc -> (env2, GenSkol tvs1 ty1 loc)
(env1, info1) = case tcTyVarDetails tv of
SkolemTv (GenSkol tvs ty loc) -> (env2, SkolemTv (GenSkol tvs1 ty1 loc))
where
(env1, tvs1) = tidyOpenTyVars env tvs
(env2, ty1) = tidyOpenType env1 ty
info -> (env, info)
pprSkolemTyVar :: TcTyVar -> SDoc
pprSkolemTyVar tv
= ASSERT( isSkolemTyVar tv )
quotes (ppr tv) <+> ptext SLIT("is bound by") <+> ppr (skolemTvInfo tv)
instance Outputable SkolemInfo where
ppr (SigSkol id) = ptext SLIT("the type signature for") <+> quotes (ppr id)
ppr (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
ppr (InstSkol df) = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
ppr (ArrowSkol loc) = ptext SLIT("the arrow form at") <+> ppr loc
ppr (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
nest 2 (ptext SLIT("at") <+> ppr loc)]
ppr (GenSkol tvs ty loc) = sep [ptext SLIT("the polymorphic type")
<+> quotes (ppr (mkForAllTys tvs ty)),
nest 2 (ptext SLIT("at") <+> ppr loc)]
pprTcTyVar :: TcTyVar -> SDoc
-- Print tyvar with info about its binding
pprTcTyVar tv
= quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv)
where
ppr_details (MetaTv _) = ptext SLIT("is a meta type variable")
ppr_details (SigSkolTv id _) = ptext SLIT("is bound by") <+> pprSkolInfo (SigSkol id)
ppr_details (SkolemTv info) = ptext SLIT("is bound by") <+> pprSkolInfo info
pprSkolInfo :: SkolemInfo -> SDoc
pprSkolInfo (SigSkol id) = ptext SLIT("the type signature for") <+> quotes (ppr id)
pprSkolInfo (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
pprSkolInfo (InstSkol df) = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
pprSkolInfo (ArrowSkol loc) = ptext SLIT("the arrow form at") <+> ppr loc
pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
nest 2 (ptext SLIT("at") <+> ppr loc)]
pprSkolInfo (GenSkol tvs ty loc) = sep [ptext SLIT("the polymorphic type")
<+> quotes (ppr (mkForAllTys tvs ty)),
nest 2 (ptext SLIT("at") <+> ppr loc)]
instance Outputable MetaDetails where
ppr Flexi = ptext SLIT("Flexi")
......@@ -319,8 +355,9 @@ isImmutableTyVar tv
isSkolemTyVar tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
SkolemTv _ -> True
MetaTv _ -> False
SkolemTv _ -> True
SigSkolTv _ _ -> True
MetaTv _ -> False
isExistentialTyVar tv -- Existential type variable, bound by a pattern
= ASSERT( isTcTyVar tv )
......@@ -331,20 +368,15 @@ isExistentialTyVar tv -- Existential type variable, bound by a pattern
isMetaTyVar tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
SkolemTv _ -> False
MetaTv _ -> True
skolemTvInfo :: TyVar -> SkolemInfo
skolemTvInfo tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
SkolemTv info -> info
other -> False
metaTvRef :: TyVar -> IORef MetaDetails
metaTvRef tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
MetaTv ref -> ref
MetaTv ref -> ref
other -> pprPanic "metaTvRef" (ppr tv)
isFlexi, isIndirect :: MetaDetails -> Bool
isFlexi Flexi = True
......
......@@ -34,9 +34,9 @@ import TypeRep ( Type(..), PredType(..), TyNote(..) )
import TcRnMonad -- TcType, amongst others
import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
TcTyVarSet, TcThetaType, Expected(..),
TcTyVarSet, TcThetaType, Expected(..), TcTyVarDetails(..),
SkolemInfo( GenSkol ), MetaDetails(..),
pprSkolemTyVar, isTauTy, isSigmaTy, mkFunTys, mkTyConApp,
pprTcTyVar, isTauTy, isSigmaTy, mkFunTys, mkTyConApp,
tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy,
......@@ -48,7 +48,7 @@ import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
isSubKind, pprKind, splitKindFunTys )
import Inst ( newDicts, instToId, tcInstCall )
import TcMType ( condLookupTcTyVar, LookupTyVarResult(..),
putMetaTyVar, tcSkolType, newKindVar, tcInstTyVars, newMetaTyVar,
tcSkolType, newKindVar, tcInstTyVars, newMetaTyVar,
newTyFlexiVarTy, zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV,
readKindVar, writeKindVar )
import TcSimplify ( tcSimplifyCheck )
......@@ -827,31 +827,57 @@ uVar swapped r1 tv1 r2 ps_ty2 ty2
case details of
IndirectTv r1' ty1 | swapped -> uTys r2 ps_ty2 ty2 r1' ty1 ty1 -- Swap back
| otherwise -> uTys r1' ty1 ty1 r2 ps_ty2 ty2 -- Same order
FlexiTv -> uFlexiVar swapped tv1 r2 ps_ty2 ty2
RigidTv -> uRigidVar swapped tv1 r2 ps_ty2 ty2
-- Expand synonyms; ignore FTVs
uFlexiVar :: Bool -> TcTyVar ->
Bool -> -- Allow refinements to ty2
TcTauType -> TcTauType -> TcM ()
-- Invariant: tv1 is Flexi
uFlexiVar swapped tv1 r2 ps_ty2 (NoteTy n2 ty2)
= uFlexiVar swapped tv1 r2 ps_ty2 ty2
uFlexiVar swapped tv1 r2 ps_ty2 ty2@(TyVarTy tv2)
DoneTv details1 -> uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
----------------
uDoneVar :: Bool -- Args are swapped
-> TcTyVar -> TcTyVarDetails -- Tyvar 1
-> Bool -- Allow refinements to ty2
-> TcTauType -> TcTauType -- Type 2
-> TcM ()
-- Invariant: tyvar 1 is not unified with anything
uDoneVar swapped tv1 details1 r2 ps_ty2 (NoteTy n2 ty2)
= -- Expand synonyms; ignore FTVs
uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
uDoneVar swapped tv1 details1 r2 ps_ty2 ty2@(TyVarTy tv2)
-- Same type variable => no-op
| tv1 == tv2
= returnM ()
-- Distinct type variables
| otherwise
= condLookupTcTyVar r2 tv2 `thenM` \ details ->
case details of
IndirectTv b ty2' -> uFlexiVar swapped tv1 b ty2' ty2'
FlexiTv | update_tv2 -> putMetaTyVar tv2 (TyVarTy tv1)
| otherwise -> updateFlexi swapped tv1 ty2
RigidTv -> updateFlexi swapped tv1 ty2
-- Note that updateFlexi does a sub-kind check
= do { lookup2 <- condLookupTcTyVar r2 tv2
; case lookup2 of
IndirectTv b ty2' -> uDoneVar swapped tv1 details1 b ty2' ty2'
DoneTv details2 -> uDoneVars swapped tv1 details1 tv2 details2
}
uDoneVar swapped tv1 details1 r2 ps_ty2 non_var_ty2 -- ty2 is not a type variable
= case details1 of
MetaTv ref1 -> do { -- Do the occurs check, and check that we are not
-- unifying a type variable with a polytype
-- Returns a zonked type ready for the update
ty2 <- checkValue tv1 r2 ps_ty2 non_var_ty2
; updateMeta swapped tv1 ref1 ty2 }
skolem_details -> unifyMisMatch (TyVarTy tv1) ps_ty2
----------------
uDoneVars :: Bool -- Args are swapped
-> TcTyVar -> TcTyVarDetails -- Tyvar 1
-> TcTyVar -> TcTyVarDetails -- Tyvar 2
-> TcM ()
-- Invarant: the type variables are distinct,
-- and are not already unified with anything
uDoneVars swapped tv1 (MetaTv ref1) tv2 details2
= case details2 of
MetaTv ref2 | update_tv2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
other -> updateMeta swapped tv1 ref1 (mkTyVarTy tv2)
-- Note that updateMeta does a sub-kind check
-- We might unify (a b) with (c d) where b::*->* and d::*; this should fail
where
k1 = tyVarKind tv1
......@@ -863,46 +889,27 @@ uFlexiVar swapped tv1 r2 ps_ty2 ty2@(TyVarTy tv2)
-- so we can choose which to do.
nicer_to_update_tv2 = isSystemName (varName tv2)
-- Try to update sys-y type variables in preference to sig-y ones
-- First one is flexi, second one isn't a type variable
uFlexiVar swapped tv1 r2 ps_ty2 non_var_ty2
= -- Do the occurs check, and check that we are not
-- unifying a type variable with a polytype
-- Returns a zonked type ready for the update
do { ty2 <- checkValue tv1 r2 ps_ty2 non_var_ty2
; updateFlexi swapped tv1 ty2 }
-- Ready to update tv1, which is flexi; occurs check is done
updateFlexi swapped tv1 ty2
= do { checkKinds swapped tv1 ty2
; putMetaTyVar tv1 ty2 }
uRigidVar :: Bool -> TcTyVar
-> Bool -> -- Allow refinements to ty2
TcTauType -> TcTauType -> TcM ()
-- Invariant: tv1 is Rigid
uRigidVar swapped tv1 r2 ps_ty2 (NoteTy n2 ty2)
= uRigidVar swapped tv1 r2 ps_ty2 ty2
-- Try to update sys-y type variables in preference to ones
-- gotten (say) by instantiating a polymorphic function with
-- a user-written type sig
uDoneVars swapped tv1 (SkolemTv _) tv2 details2
= case details2 of
MetaTv ref2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
other -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2)
-- The both-type-variable case
uRigidVar swapped tv1 r2 ps_ty2 ty2@(TyVarTy tv2)
-- Same type variable => no-op
| tv1 == tv2
= returnM ()
uDoneVars swapped tv1 (SigSkolTv _ ref1) tv2 details2
= case details2 of
MetaTv ref2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
SigSkolTv _ _ -> updateMeta swapped tv1 ref1 (mkTyVarTy tv2)
other -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2)
-- Distinct type variables
| otherwise
= condLookupTcTyVar r2 tv2 `thenM` \ details ->
case details of
IndirectTv b ty2' -> uRigidVar swapped tv1 b ty2' ty2'
FlexiTv -> updateFlexi swapped tv2 (TyVarTy tv1)
RigidTv -> unifyMisMatch (TyVarTy tv1) (TyVarTy tv2)
-- Second one isn't a type variable
uRigidVar swapped tv1 r2 ps_ty2 non_var_ty2
= unifyMisMatch (TyVarTy tv1) ps_ty2
----------------
updateMeta :: Bool -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
-- Update tv1, which is flexi; occurs check is alrady done
updateMeta swapped tv1 ref1 ty2
= do { checkKinds swapped tv1 ty2
; writeMutVar ref1 (Indirect ty2) }
\end{code}
\begin{code}
......@@ -919,7 +926,6 @@ checkKinds swapped tv1 ty2
-- unlifted type: e.g. (id 3#) is illegal
= addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
unifyKindMisMatch k1 k2
where
(k1,k2) | swapped = (tk2,tk1)
| otherwise = (tk1,tk2)
......@@ -1186,7 +1192,7 @@ ppr_ty env ty
; case tidy_ty of
TyVarTy tv
| isSkolemTyVar tv -> return (env2, pp_rigid tv',
pprSkolemTyVar tv')
pprTcTyVar tv')
| otherwise -> return simple_result
where
(env2, tv') = tidySkolemTyVar env1 tv
......