Commit 7e1c492d authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Typechecker comments and debug tracing only

parent af33073c
......@@ -722,7 +722,7 @@ yields a better error message anyway.)
flatten :: FlattenMode -> CtEvidence -> TcType
-> TcS (Xi, TcCoercion)
flatten mode ev ty
= do { traceTcS "flatten {" (ppr ty)
= do { traceTcS "flatten {" (ppr mode <+> ppr ty)
; (ty', co) <- runFlatten mode ev (flatten_one ty)
; traceTcS "flatten }" (ppr ty')
; return (ty', co) }
......
......@@ -1026,7 +1026,9 @@ zonkQuantifiedTyVar default_kind tv
= do { tv' <- skolemiseUnboundMetaTyVar tv
; return (Just tv') }
where
-- do not default SigTvs. This would violate the invariants on SigTvs
-- Do not default SigTvs. Doing so would violate the invariants
-- on SigTvs; see Note [Signature skolems] in TcType.
-- Trac #13343 is an example
not_sig_tv = case info of SigTv -> False
_ -> True
......
......@@ -439,15 +439,23 @@ why Var.hs shouldn't actually have the definition, but it "belongs" here.
Note [Signature skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
A SigTv is a specialised variant of TauTv, with the following invarints:
* A SigTv can be unified only with a TyVar,
not with any other type
* Its MetaDetails, if filled in, will always be another SigTv
or a SkolemTv
SigTvs are only distinguished to improve error messages.
Consider this
f :: forall a. [a] -> Int
f (x::b : xs) = 3
Here 'b' is a lexically scoped type variable, but it turns out to be
the same as the skolem 'a'. So we have a special kind of skolem
constant, SigTv, which can unify with other SigTvs. They are used
*only* for pattern type signatures.
the same as the skolem 'a'. So we make them both SigTvs, which can unify
with each other.
Similarly consider
data T (a:k1) = MkT (S a)
......@@ -455,6 +463,8 @@ Similarly consider
When doing kind inference on {S,T} we don't want *skolems* for k1,k2,
because they end up unifying; we want those SigTvs again.
SigTvs are used *only* for pattern type signatures.
Note [TyVars and TcTyVars during type checking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The Var type has constructors TyVar and TcTyVar. They are used
......@@ -514,10 +524,7 @@ data MetaInfo
| SigTv -- A variant of TauTv, except that it should not be
-- unified with a type, only with a type variable
-- SigTvs are only distinguished to improve error messages
-- see Note [Signature skolems]
-- The MetaDetails, if filled in, will
-- always be another SigTv or a SkolemTv
-- See Note [Signature skolems]
| FlatMetaTv -- A flatten meta-tyvar
-- It is a meta-tyvar, but it is always untouchable, with level 0
......
......@@ -1908,8 +1908,7 @@ metaTyVarUpdateOK :: DynFlags
-> TcType -- ty :: k2
-> Maybe TcType -- possibly-expanded ty
-- (metaTyFVarUpdateOK tv ty)
-- We are about to update the meta-tyvar tv with ty, in
-- our on-the-flyh unifier
-- We are about to update the meta-tyvar tv with ty
-- Check (a) that tv doesn't occur in ty (occurs check)
-- (b) that ty does not have any foralls
-- (in the impredicative case), or type functions
......
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