Improve typechecking of RULEs, to account for type wildcard holes
[ghc.git] / compiler / typecheck / TcMType.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5
6 Monadic type operations
7
8 This module contains monadic operations over types that contain
9 mutable type variables
10 -}
11
12 {-# LANGUAGE CPP #-}
13
14 module TcMType (
15 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
16
17 --------------------------------
18 -- Creating new mutable type variables
19 newFlexiTyVar,
20 newFlexiTyVarTy, -- Kind -> TcM TcType
21 newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
22 newReturnTyVar, newReturnTyVarTy,
23 newMetaKindVar, newMetaKindVars,
24 mkTcTyVarName, cloneMetaTyVar,
25
26 newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
27 newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
28
29 --------------------------------
30 -- Creating new evidence variables
31 newEvVar, newEvVars, newEq, newDict,
32 newTcEvBinds, addTcEvBind,
33
34 --------------------------------
35 -- Instantiation
36 tcInstTyVars, tcInstTyVarX, newSigTyVar,
37 tcInstType,
38 tcInstSkolTyVars, tcInstSuperSkolTyVarsX,
39 tcInstSigTyVarsLoc, tcInstSigTyVars,
40 tcInstSkolType,
41 tcSkolDFunType, tcSuperSkolTyVars,
42
43 instSkolTyVars, freshenTyVarBndrs,
44
45 --------------------------------
46 -- Zonking and tidying
47 zonkTcPredType, zonkTidyTcType, zonkTidyOrigin,
48 tidyEvVar, tidyCt, tidySkolemInfo,
49 skolemiseUnboundMetaTyVar,
50 zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, zonkTcTypeAndFV,
51 zonkQuantifiedTyVar, quantifyTyVars,
52 zonkTcTyVarBndr, zonkTcType, zonkTcTypes, zonkTcThetaType,
53
54 zonkTcKind, defaultKindVarToStar,
55 zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo,
56
57 tcGetGlobalTyVars,
58
59 --------------------------------
60 -- (Named) Wildcards
61 newWildcardVar, newWildcardVarMetaKind
62 ) where
63
64 #include "HsVersions.h"
65
66 -- friends:
67 import TypeRep
68 import TcType
69 import Type
70 import Class
71 import Var
72 import VarEnv
73
74 -- others:
75 import TcRnMonad -- TcType, amongst others
76 import Id
77 import Name
78 import VarSet
79 import PrelNames
80 import DynFlags
81 import Util
82 import Outputable
83 import FastString
84 import SrcLoc
85 import Bag
86
87 import Control.Monad
88 import Data.List ( partition, mapAccumL )
89
90 {-
91 ************************************************************************
92 * *
93 Kind variables
94 * *
95 ************************************************************************
96 -}
97
98 mkKindName :: Unique -> Name
99 mkKindName unique = mkSystemName unique kind_var_occ
100
101 kind_var_occ :: OccName -- Just one for all MetaKindVars
102 -- They may be jiggled by tidying
103 kind_var_occ = mkOccName tvName "k"
104
105 newMetaKindVar :: TcM TcKind
106 newMetaKindVar = do { uniq <- newUnique
107 ; details <- newMetaDetails (TauTv False)
108 ; let kv = mkTcTyVar (mkKindName uniq) superKind details
109 ; return (mkTyVarTy kv) }
110
111 newMetaKindVars :: Int -> TcM [TcKind]
112 newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
113
114 {-
115 ************************************************************************
116 * *
117 Evidence variables; range over constraints we can abstract over
118 * *
119 ************************************************************************
120 -}
121
122 newEvVars :: TcThetaType -> TcM [EvVar]
123 newEvVars theta = mapM newEvVar theta
124
125 --------------
126
127 newEvVar :: TcPredType -> TcM EvVar
128 -- Creates new *rigid* variables for predicates
129 newEvVar ty = do { name <- newSysName (predTypeOccName ty)
130 ; return (mkLocalId name ty) }
131
132 newEq :: TcType -> TcType -> TcM EvVar
133 newEq ty1 ty2
134 = do { name <- newSysName (mkVarOccFS (fsLit "cobox"))
135 ; return (mkLocalId name (mkTcEqPred ty1 ty2)) }
136
137 newDict :: Class -> [TcType] -> TcM DictId
138 newDict cls tys
139 = do { name <- newSysName (mkDictOcc (getOccName cls))
140 ; return (mkLocalId name (mkClassPred cls tys)) }
141
142 predTypeOccName :: PredType -> OccName
143 predTypeOccName ty = case classifyPredType ty of
144 ClassPred cls _ -> mkDictOcc (getOccName cls)
145 EqPred _ _ _ -> mkVarOccFS (fsLit "cobox")
146 TuplePred _ -> mkVarOccFS (fsLit "tup")
147 IrredPred _ -> mkVarOccFS (fsLit "irred")
148
149
150 {-
151 ************************************************************************
152 * *
153 SkolemTvs (immutable)
154 * *
155 ************************************************************************
156 -}
157
158 tcInstType :: ([TyVar] -> TcM (TvSubst, [TcTyVar])) -- How to instantiate the type variables
159 -> TcType -- Type to instantiate
160 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
161 -- (type vars (excl coercion vars), preds (incl equalities), rho)
162 tcInstType inst_tyvars ty
163 = case tcSplitForAllTys ty of
164 ([], rho) -> let -- There may be overloading despite no type variables;
165 -- (?x :: Int) => Int -> Int
166 (theta, tau) = tcSplitPhiTy rho
167 in
168 return ([], theta, tau)
169
170 (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
171 ; let (theta, tau) = tcSplitPhiTy (substTy subst rho)
172 ; return (tyvars', theta, tau) }
173
174 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
175 -- Instantiate a type signature with skolem constants.
176 -- We could give them fresh names, but no need to do so
177 tcSkolDFunType ty = tcInstType tcInstSuperSkolTyVars ty
178
179 tcSuperSkolTyVars :: [TyVar] -> (TvSubst, [TcTyVar])
180 -- Make skolem constants, but do *not* give them new names, as above
181 -- Moreover, make them "super skolems"; see comments with superSkolemTv
182 -- see Note [Kind substitution when instantiating]
183 -- Precondition: tyvars should be ordered (kind vars first)
184 tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar (mkTopTvSubst [])
185
186 tcSuperSkolTyVar :: TvSubst -> TyVar -> (TvSubst, TcTyVar)
187 tcSuperSkolTyVar subst tv
188 = (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv)
189 where
190 kind = substTy subst (tyVarKind tv)
191 new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
192
193 tcInstSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
194 tcInstSkolTyVars = tcInstSkolTyVars' False emptyTvSubst
195
196 tcInstSuperSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
197 tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTvSubst
198
199 tcInstSuperSkolTyVarsX :: TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
200 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
201
202 tcInstSkolTyVars' :: Bool -> TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
203 -- Precondition: tyvars should be ordered (kind vars first)
204 -- see Note [Kind substitution when instantiating]
205 -- Get the location from the monad; this is a complete freshening operation
206 tcInstSkolTyVars' overlappable subst tvs
207 = do { loc <- getSrcSpanM
208 ; instSkolTyVarsX (mkTcSkolTyVar loc overlappable) subst tvs }
209
210 mkTcSkolTyVar :: SrcSpan -> Bool -> Unique -> Name -> Kind -> TcTyVar
211 mkTcSkolTyVar loc overlappable uniq old_name kind
212 = mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
213 kind
214 (SkolemTv overlappable)
215
216 tcInstSigTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
217 -- We specify the location
218 tcInstSigTyVarsLoc loc = instSkolTyVars (mkTcSkolTyVar loc False)
219
220 tcInstSigTyVars :: [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
221 -- Get the location from the TyVar itself, not the monad
222 tcInstSigTyVars
223 = instSkolTyVars mk_tv
224 where
225 mk_tv uniq old_name kind
226 = mkTcTyVar (setNameUnique old_name uniq) kind (SkolemTv False)
227
228 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
229 -- Instantiate a type with fresh skolem constants
230 -- Binding location comes from the monad
231 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
232
233 ------------------
234 freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
235 -- ^ Give fresh uniques to a bunch of TyVars, but they stay
236 -- as TyVars, rather than becoming TcTyVars
237 -- Used in FamInst.newFamInst, and Inst.newClsInst
238 freshenTyVarBndrs = instSkolTyVars mk_tv
239 where
240 mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
241
242 ------------------
243 instSkolTyVars :: (Unique -> Name -> Kind -> TyVar)
244 -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
245 instSkolTyVars mk_tv = instSkolTyVarsX mk_tv emptyTvSubst
246
247 instSkolTyVarsX :: (Unique -> Name -> Kind -> TyVar)
248 -> TvSubst -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
249 instSkolTyVarsX mk_tv = mapAccumLM (instSkolTyVarX mk_tv)
250
251 instSkolTyVarX :: (Unique -> Name -> Kind -> TyVar)
252 -> TvSubst -> TyVar -> TcRnIf gbl lcl (TvSubst, TyVar)
253 instSkolTyVarX mk_tv subst tyvar
254 = do { uniq <- newUnique
255 ; let new_tv = mk_tv uniq old_name kind
256 ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
257 where
258 old_name = tyVarName tyvar
259 kind = substTy subst (tyVarKind tyvar)
260
261 {-
262 Note [Kind substitution when instantiating]
263 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
264 When we instantiate a bunch of kind and type variables, first we
265 expect them to be sorted (kind variables first, then type variables).
266 Then we have to instantiate the kind variables, build a substitution
267 from old variables to the new variables, then instantiate the type
268 variables substituting the original kind.
269
270 Exemple: If we want to instantiate
271 [(k1 :: BOX), (k2 :: BOX), (a :: k1 -> k2), (b :: k1)]
272 we want
273 [(?k1 :: BOX), (?k2 :: BOX), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
274 instead of the buggous
275 [(?k1 :: BOX), (?k2 :: BOX), (?a :: k1 -> k2), (?b :: k1)]
276
277
278 ************************************************************************
279 * *
280 MetaTvs (meta type variables; mutable)
281 * *
282 ************************************************************************
283 -}
284
285 newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
286 -- Make a new meta tyvar out of thin air
287 newMetaTyVar meta_info kind
288 = do { uniq <- newUnique
289 ; let name = mkTcTyVarName uniq s
290 s = case meta_info of
291 ReturnTv -> fsLit "r"
292 TauTv True -> fsLit "w"
293 TauTv False -> fsLit "t"
294 FlatMetaTv -> fsLit "fmv"
295 SigTv -> fsLit "a"
296 ; details <- newMetaDetails meta_info
297 ; return (mkTcTyVar name kind details) }
298
299 newNamedMetaTyVar :: Name -> MetaInfo -> Kind -> TcM TcTyVar
300 -- Make a new meta tyvar out of thin air
301 newNamedMetaTyVar name meta_info kind
302 = do { details <- newMetaDetails meta_info
303 ; return (mkTcTyVar name kind details) }
304
305 newSigTyVar :: Name -> Kind -> TcM TcTyVar
306 newSigTyVar name kind
307 = do { uniq <- newUnique
308 ; let name' = setNameUnique name uniq
309 -- Use the same OccName so that the tidy-er
310 -- doesn't gratuitously rename 'a' to 'a0' etc
311 ; details <- newMetaDetails SigTv
312 ; return (mkTcTyVar name' kind details) }
313
314 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
315 newMetaDetails info
316 = do { ref <- newMutVar Flexi
317 ; tclvl <- getTcLevel
318 ; return (MetaTv { mtv_info = info, mtv_ref = ref, mtv_tclvl = tclvl }) }
319
320 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
321 cloneMetaTyVar tv
322 = ASSERT( isTcTyVar tv )
323 do { uniq <- newUnique
324 ; ref <- newMutVar Flexi
325 ; let name' = setNameUnique (tyVarName tv) uniq
326 details' = case tcTyVarDetails tv of
327 details@(MetaTv {}) -> details { mtv_ref = ref }
328 _ -> pprPanic "cloneMetaTyVar" (ppr tv)
329 ; return (mkTcTyVar name' (tyVarKind tv) details') }
330
331 mkTcTyVarName :: Unique -> FastString -> Name
332 -- Make sure that fresh TcTyVar names finish with a digit
333 -- leaving the un-cluttered names free for user names
334 mkTcTyVarName uniq str = mkSysTvName uniq str
335
336 -- Works for both type and kind variables
337 readMetaTyVar :: TyVar -> TcM MetaDetails
338 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
339 readMutVar (metaTvRef tyvar)
340
341 isFilledMetaTyVar :: TyVar -> TcM Bool
342 -- True of a filled-in (Indirect) meta type variable
343 isFilledMetaTyVar tv
344 | not (isTcTyVar tv) = return False
345 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
346 = do { details <- readMutVar ref
347 ; return (isIndirect details) }
348 | otherwise = return False
349
350 isUnfilledMetaTyVar :: TyVar -> TcM Bool
351 -- True of a un-filled-in (Flexi) meta type variable
352 isUnfilledMetaTyVar tv
353 | not (isTcTyVar tv) = return False
354 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
355 = do { details <- readMutVar ref
356 ; return (isFlexi details) }
357 | otherwise = return False
358
359 --------------------
360 -- Works with both type and kind variables
361 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
362 -- Write into a currently-empty MetaTyVar
363
364 writeMetaTyVar tyvar ty
365 | not debugIsOn
366 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
367
368 -- Everything from here on only happens if DEBUG is on
369 | not (isTcTyVar tyvar)
370 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
371 return ()
372
373 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
374 = writeMetaTyVarRef tyvar ref ty
375
376 | otherwise
377 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
378 return ()
379
380 --------------------
381 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
382 -- Here the tyvar is for error checking only;
383 -- the ref cell must be for the same tyvar
384 writeMetaTyVarRef tyvar ref ty
385 | not debugIsOn
386 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
387 ; writeMutVar ref (Indirect ty) }
388
389 -- Everything from here on only happens if DEBUG is on
390 | otherwise
391 = do { meta_details <- readMutVar ref;
392 -- Zonk kinds to allow the error check to work
393 ; zonked_tv_kind <- zonkTcKind tv_kind
394 ; zonked_ty_kind <- zonkTcKind ty_kind
395
396 -- Check for double updates
397 ; ASSERT2( isFlexi meta_details,
398 hang (text "Double update of meta tyvar")
399 2 (ppr tyvar $$ ppr meta_details) )
400
401 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
402 ; writeMutVar ref (Indirect ty)
403 ; when ( not (isPredTy tv_kind)
404 -- Don't check kinds for updates to coercion variables
405 && not (zonked_ty_kind `tcIsSubKind` zonked_tv_kind))
406 $ WARN( True, hang (text "Ill-kinded update to meta tyvar")
407 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
408 <+> text ":="
409 <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) ) )
410 (return ()) }
411 where
412 tv_kind = tyVarKind tyvar
413 ty_kind = typeKind ty
414
415 {-
416 ************************************************************************
417 * *
418 MetaTvs: TauTvs
419 * *
420 ************************************************************************
421 -}
422
423 newFlexiTyVar :: Kind -> TcM TcTyVar
424 newFlexiTyVar kind = newMetaTyVar (TauTv False) kind
425
426 newFlexiTyVarTy :: Kind -> TcM TcType
427 newFlexiTyVarTy kind = do
428 tc_tyvar <- newFlexiTyVar kind
429 return (TyVarTy tc_tyvar)
430
431 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
432 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
433
434 newReturnTyVar :: Kind -> TcM TcTyVar
435 newReturnTyVar kind = newMetaTyVar ReturnTv kind
436
437 newReturnTyVarTy :: Kind -> TcM TcType
438 newReturnTyVarTy kind = TyVarTy <$> newReturnTyVar kind
439
440 tcInstTyVars :: [TKVar] -> TcM (TvSubst, [TcTyVar])
441 -- Instantiate with META type variables
442 -- Note that this works for a sequence of kind and type
443 -- variables. Eg [ (k:BOX), (a:k->k) ]
444 -- Gives [ (k7:BOX), (a8:k7->k7) ]
445 tcInstTyVars tyvars = mapAccumLM tcInstTyVarX emptyTvSubst tyvars
446 -- emptyTvSubst has an empty in-scope set, but that's fine here
447 -- Since the tyvars are freshly made, they cannot possibly be
448 -- captured by any existing for-alls.
449
450 tcInstTyVarX :: TvSubst -> TKVar -> TcM (TvSubst, TcTyVar)
451 -- Make a new unification variable tyvar whose Name and Kind come from
452 -- an existing TyVar. We substitute kind variables in the kind.
453 tcInstTyVarX subst tyvar
454 = do { uniq <- newUnique
455 ; details <- newMetaDetails (TauTv False)
456 ; let name = mkSystemName uniq (getOccName tyvar)
457 kind = substTy subst (tyVarKind tyvar)
458 new_tv = mkTcTyVar name kind details
459 ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
460
461 {-
462 ************************************************************************
463 * *
464 Quantification
465 * *
466 ************************************************************************
467
468 Note [quantifyTyVars]
469 ~~~~~~~~~~~~~~~~~~~~~
470 quantifyTyVars is give the free vars of a type that we
471 are about to wrap in a forall.
472
473 It takes these free type/kind variables and
474 1. Zonks them and remove globals
475 2. Partitions into type and kind variables (kvs1, tvs)
476 3. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
477 4. Calls zonkQuantifiedTyVar on each
478
479 Step (3) is often unimportant, because the kind variable is often
480 also free in the type. Eg
481 Typeable k (a::k)
482 has free vars {k,a}. But the type (see Trac #7916)
483 (f::k->*) (a::k)
484 has free vars {f,a}, but we must add 'k' as well! Hence step (3).
485 -}
486
487 quantifyTyVars :: TcTyVarSet -> TcTyVarSet -> TcM [TcTyVar]
488 -- See Note [quantifyTyVars]
489 -- The input is a mixture of type and kind variables; a kind variable k
490 -- may occur *after* a tyvar mentioning k in its kind
491 -- Can be given a mixture of TcTyVars and TyVars, in the case of
492 -- associated type declarations
493
494 quantifyTyVars gbl_tvs tkvs
495 = do { tkvs <- zonkTyVarsAndFV tkvs
496 ; gbl_tvs <- zonkTyVarsAndFV gbl_tvs
497 ; let (kvs, tvs) = partitionVarSet isKindVar (closeOverKinds tkvs `minusVarSet` gbl_tvs)
498 -- NB kinds of tvs are zonked by zonkTyVarsAndFV
499 kvs2 = varSetElems kvs
500 qtvs = varSetElems tvs
501
502 -- In the non-PolyKinds case, default the kind variables
503 -- to *, and zonk the tyvars as usual. Notice that this
504 -- may make quantifyTyVars return a shorter list
505 -- than it was passed, but that's ok
506 ; poly_kinds <- xoptM Opt_PolyKinds
507 ; qkvs <- if poly_kinds
508 then return kvs2
509 else do { let (meta_kvs, skolem_kvs) = partition is_meta kvs2
510 is_meta kv = isTcTyVar kv && isMetaTyVar kv
511 ; mapM_ defaultKindVarToStar meta_kvs
512 ; return skolem_kvs } -- should be empty
513
514 ; mapM zonk_quant (qkvs ++ qtvs) }
515 -- Because of the order, any kind variables
516 -- mentioned in the kinds of the type variables refer to
517 -- the now-quantified versions
518 where
519 zonk_quant tkv
520 | isTcTyVar tkv = zonkQuantifiedTyVar tkv
521 | otherwise = return tkv
522 -- For associated types, we have the class variables
523 -- in scope, and they are TyVars not TcTyVars
524
525 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
526 -- The quantified type variables often include meta type variables
527 -- we want to freeze them into ordinary type variables, and
528 -- default their kind (e.g. from OpenTypeKind to TypeKind)
529 -- -- see notes with Kind.defaultKind
530 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
531 -- bound occurrences of the original type variable will get zonked to
532 -- the immutable version.
533 --
534 -- We leave skolem TyVars alone; they are immutable.
535 --
536 -- This function is called on both kind and type variables,
537 -- but kind variables *only* if PolyKinds is on.
538 zonkQuantifiedTyVar tv
539 = ASSERT2( isTcTyVar tv, ppr tv )
540 case tcTyVarDetails tv of
541 SkolemTv {} -> do { kind <- zonkTcKind (tyVarKind tv)
542 ; return $ setTyVarKind tv kind }
543 -- It might be a skolem type variable,
544 -- for example from a user type signature
545
546 MetaTv { mtv_ref = ref } ->
547 do when debugIsOn $ do
548 -- [Sept 04] Check for non-empty.
549 -- See note [Silly Type Synonym]
550 cts <- readMutVar ref
551 case cts of
552 Flexi -> return ()
553 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
554 return ()
555 skolemiseUnboundMetaTyVar tv vanillaSkolemTv
556 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
557
558 defaultKindVarToStar :: TcTyVar -> TcM Kind
559 -- We have a meta-kind: unify it with '*'
560 defaultKindVarToStar kv
561 = do { ASSERT( isKindVar kv && isMetaTyVar kv )
562 writeMetaTyVar kv liftedTypeKind
563 ; return liftedTypeKind }
564
565 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
566 -- We have a Meta tyvar with a ref-cell inside it
567 -- Skolemise it, including giving it a new Name, so that
568 -- we are totally out of Meta-tyvar-land
569 -- We create a skolem TyVar, not a regular TyVar
570 -- See Note [Zonking to Skolem]
571 skolemiseUnboundMetaTyVar tv details
572 = ASSERT2( isMetaTyVar tv, ppr tv )
573 do { span <- getSrcSpanM -- Get the location from "here"
574 -- ie where we are generalising
575 ; uniq <- newUnique -- Remove it from TcMetaTyVar unique land
576 ; kind <- zonkTcKind (tyVarKind tv)
577 ; let tv_name = getOccName tv
578 new_tv_name = if isWildcardVar tv
579 then generaliseWildcardVarName tv_name
580 else tv_name
581 final_name = mkInternalName uniq new_tv_name span
582 final_kind = defaultKind kind
583 final_tv = mkTcTyVar final_name final_kind details
584
585 ; traceTc "Skolemising" (ppr tv <+> ptext (sLit ":=") <+> ppr final_tv)
586 ; writeMetaTyVar tv (mkTyVarTy final_tv)
587 ; return final_tv }
588 where
589 -- If a wildcard type called _a is generalised, we rename it to w_a
590 generaliseWildcardVarName :: OccName -> OccName
591 generaliseWildcardVarName name | startsWithUnderscore name
592 = mkOccNameFS (occNameSpace name) (appendFS (fsLit "w") (occNameFS name))
593 generaliseWildcardVarName name = name
594
595 {-
596 Note [Zonking to Skolem]
597 ~~~~~~~~~~~~~~~~~~~~~~~~
598 We used to zonk quantified type variables to regular TyVars. However, this
599 leads to problems. Consider this program from the regression test suite:
600
601 eval :: Int -> String -> String -> String
602 eval 0 root actual = evalRHS 0 root actual
603
604 evalRHS :: Int -> a
605 evalRHS 0 root actual = eval 0 root actual
606
607 It leads to the deferral of an equality (wrapped in an implication constraint)
608
609 forall a. () => ((String -> String -> String) ~ a)
610
611 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
612 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
613 This has the *side effect* of also zonking the `a' in the deferred equality
614 (which at this point is being handed around wrapped in an implication
615 constraint).
616
617 Finally, the equality (with the zonked `a') will be handed back to the
618 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
619 If we zonk `a' with a regular type variable, we will have this regular type
620 variable now floating around in the simplifier, which in many places assumes to
621 only see proper TcTyVars.
622
623 We can avoid this problem by zonking with a skolem. The skolem is rigid
624 (which we require for a quantified variable), but is still a TcTyVar that the
625 simplifier knows how to deal with.
626
627 Note [Silly Type Synonyms]
628 ~~~~~~~~~~~~~~~~~~~~~~~~~~
629 Consider this:
630 type C u a = u -- Note 'a' unused
631
632 foo :: (forall a. C u a -> C u a) -> u
633 foo x = ...
634
635 bar :: Num u => u
636 bar = foo (\t -> t + t)
637
638 * From the (\t -> t+t) we get type {Num d} => d -> d
639 where d is fresh.
640
641 * Now unify with type of foo's arg, and we get:
642 {Num (C d a)} => C d a -> C d a
643 where a is fresh.
644
645 * Now abstract over the 'a', but float out the Num (C d a) constraint
646 because it does not 'really' mention a. (see exactTyVarsOfType)
647 The arg to foo becomes
648 \/\a -> \t -> t+t
649
650 * So we get a dict binding for Num (C d a), which is zonked to give
651 a = ()
652 [Note Sept 04: now that we are zonking quantified type variables
653 on construction, the 'a' will be frozen as a regular tyvar on
654 quantification, so the floated dict will still have type (C d a).
655 Which renders this whole note moot; happily!]
656
657 * Then the \/\a abstraction has a zonked 'a' in it.
658
659 All very silly. I think its harmless to ignore the problem. We'll end up with
660 a \/\a in the final result but all the occurrences of a will be zonked to ()
661
662 ************************************************************************
663 * *
664 Zonking types
665 * *
666 ************************************************************************
667
668 @tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
669 To improve subsequent calls to the same function it writes the zonked set back into
670 the environment.
671 -}
672
673 tcGetGlobalTyVars :: TcM TcTyVarSet
674 tcGetGlobalTyVars
675 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
676 ; gbl_tvs <- readMutVar gtv_var
677 ; gbl_tvs' <- zonkTyVarsAndFV gbl_tvs
678 ; writeMutVar gtv_var gbl_tvs'
679 ; return gbl_tvs' }
680 where
681
682 zonkTcTypeAndFV :: TcType -> TcM TyVarSet
683 -- Zonk a type and take its free variables
684 -- With kind polymorphism it can be essential to zonk *first*
685 -- so that we find the right set of free variables. Eg
686 -- forall k1. forall (a:k2). a
687 -- where k2:=k1 is in the substitution. We don't want
688 -- k2 to look free in this type!
689 zonkTcTypeAndFV ty = do { ty <- zonkTcType ty; return (tyVarsOfType ty) }
690
691 zonkTyVar :: TyVar -> TcM TcType
692 -- Works on TyVars and TcTyVars
693 zonkTyVar tv | isTcTyVar tv = zonkTcTyVar tv
694 | otherwise = return (mkTyVarTy tv)
695 -- Hackily, when typechecking type and class decls
696 -- we have TyVars in scopeadded (only) in
697 -- TcHsType.tcTyClTyVars, but it seems
698 -- painful to make them into TcTyVars there
699
700 zonkTyVarsAndFV :: TyVarSet -> TcM TyVarSet
701 zonkTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTyVar (varSetElems tyvars)
702
703 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
704 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
705
706 ----------------- Types
707 zonkTyVarKind :: TyVar -> TcM TyVar
708 zonkTyVarKind tv = do { kind' <- zonkTcKind (tyVarKind tv)
709 ; return (setTyVarKind tv kind') }
710
711 zonkTcTypes :: [TcType] -> TcM [TcType]
712 zonkTcTypes tys = mapM zonkTcType tys
713
714 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
715 zonkTcThetaType theta = mapM zonkTcPredType theta
716
717 zonkTcPredType :: TcPredType -> TcM TcPredType
718 zonkTcPredType = zonkTcType
719
720 {-
721 ************************************************************************
722 * *
723 Zonking constraints
724 * *
725 ************************************************************************
726 -}
727
728 zonkImplication :: Implication -> TcM Implication
729 zonkImplication implic@(Implic { ic_skols = skols
730 , ic_given = given
731 , ic_wanted = wanted
732 , ic_info = info })
733 = do { skols' <- mapM zonkTcTyVarBndr skols -- Need to zonk their kinds!
734 -- as Trac #7230 showed
735 ; given' <- mapM zonkEvVar given
736 ; info' <- zonkSkolemInfo info
737 ; wanted' <- zonkWCRec wanted
738 ; return (implic { ic_skols = skols'
739 , ic_given = given'
740 , ic_wanted = wanted'
741 , ic_info = info' }) }
742
743 zonkEvVar :: EvVar -> TcM EvVar
744 zonkEvVar var = do { ty' <- zonkTcType (varType var)
745 ; return (setVarType var ty') }
746
747
748 zonkWC :: WantedConstraints -> TcM WantedConstraints
749 zonkWC wc = zonkWCRec wc
750
751 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
752 zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
753 = do { simple' <- zonkSimples simple
754 ; implic' <- mapBagM zonkImplication implic
755 ; insol' <- zonkSimples insol
756 ; return (WC { wc_simple = simple', wc_impl = implic', wc_insol = insol' }) }
757
758 zonkSimples :: Cts -> TcM Cts
759 zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
760 ; traceTc "zonkSimples done:" (ppr cts')
761 ; return cts' }
762
763 zonkCt' :: Ct -> TcM Ct
764 zonkCt' ct = zonkCt ct
765
766 zonkCt :: Ct -> TcM Ct
767 zonkCt ct@(CHoleCan { cc_ev = ev })
768 = do { ev' <- zonkCtEvidence ev
769 ; return $ ct { cc_ev = ev' } }
770 zonkCt ct
771 = do { fl' <- zonkCtEvidence (cc_ev ct)
772 ; return (mkNonCanonical fl') }
773
774 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
775 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
776 = do { pred' <- zonkTcType pred
777 ; return (ctev { ctev_pred = pred'}) }
778 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred })
779 = do { pred' <- zonkTcType pred
780 ; return (ctev { ctev_pred = pred' }) }
781 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
782 = do { pred' <- zonkTcType pred
783 ; return (ctev { ctev_pred = pred' }) }
784
785 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
786 zonkSkolemInfo (SigSkol cx ty) = do { ty' <- zonkTcType ty
787 ; return (SigSkol cx ty') }
788 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
789 ; return (InferSkol ntys') }
790 where
791 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
792 zonkSkolemInfo skol_info = return skol_info
793
794 {-
795 ************************************************************************
796 * *
797 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
798 * *
799 * For internal use only! *
800 * *
801 ************************************************************************
802 -}
803
804 -- zonkId is used *during* typechecking just to zonk the Id's type
805 zonkId :: TcId -> TcM TcId
806 zonkId id
807 = do { ty' <- zonkTcType (idType id)
808 ; return (Id.setIdType id ty') }
809
810 -- For unbound, mutable tyvars, zonkType uses the function given to it
811 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
812 -- type variable and zonks the kind too
813
814 zonkTcType :: TcType -> TcM TcType
815 zonkTcType ty
816 = go ty
817 where
818 go (TyConApp tc tys) = do tys' <- mapM go tys
819 return (TyConApp tc tys')
820 -- Do NOT establish Type invariants, because
821 -- doing so is strict in the TyCOn.
822 -- See Note [Zonking inside the knot] in TcHsType
823
824 go (LitTy n) = return (LitTy n)
825
826 go (FunTy arg res) = do arg' <- go arg
827 res' <- go res
828 return (FunTy arg' res')
829
830 go (AppTy fun arg) = do fun' <- go fun
831 arg' <- go arg
832 return (mkAppTy fun' arg')
833 -- NB the mkAppTy; we might have instantiated a
834 -- type variable to a type constructor, so we need
835 -- to pull the TyConApp to the top.
836 -- OK to do this because only strict in the structure
837 -- not in the TyCon.
838 -- See Note [Zonking inside the knot] in TcHsType
839
840 -- The two interesting cases!
841 go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar
842 | otherwise = TyVarTy <$> updateTyVarKindM go tyvar
843 -- Ordinary (non Tc) tyvars occur inside quantified types
844
845 go (ForAllTy tv ty) = do { tv' <- zonkTcTyVarBndr tv
846 ; ty' <- go ty
847 ; return (ForAllTy tv' ty') }
848
849 zonkTcTyVarBndr :: TcTyVar -> TcM TcTyVar
850 -- A tyvar binder is never a unification variable (MetaTv),
851 -- rather it is always a skolems. BUT it may have a kind
852 -- that has not yet been zonked, and may include kind
853 -- unification variables.
854 zonkTcTyVarBndr tyvar
855 = ASSERT2( isImmutableTyVar tyvar, ppr tyvar ) do
856 updateTyVarKindM zonkTcType tyvar
857
858 zonkTcTyVar :: TcTyVar -> TcM TcType
859 -- Simply look through all Flexis
860 zonkTcTyVar tv
861 = ASSERT2( isTcTyVar tv, ppr tv ) do
862 case tcTyVarDetails tv of
863 SkolemTv {} -> zonk_kind_and_return
864 RuntimeUnk {} -> zonk_kind_and_return
865 FlatSkol ty -> zonkTcType ty
866 MetaTv { mtv_ref = ref }
867 -> do { cts <- readMutVar ref
868 ; case cts of
869 Flexi -> zonk_kind_and_return
870 Indirect ty -> zonkTcType ty }
871 where
872 zonk_kind_and_return = do { z_tv <- zonkTyVarKind tv
873 ; return (TyVarTy z_tv) }
874
875 {-
876 ************************************************************************
877 * *
878 Zonking kinds
879 * *
880 ************************************************************************
881 -}
882
883 zonkTcKind :: TcKind -> TcM TcKind
884 zonkTcKind k = zonkTcType k
885
886 {-
887 ************************************************************************
888 * *
889 Tidying
890 * *
891 ************************************************************************
892 -}
893
894 zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
895 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
896 ; return (tidyOpenType env ty') }
897
898 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
899 zonkTidyOrigin env (GivenOrigin skol_info)
900 = do { skol_info1 <- zonkSkolemInfo skol_info
901 ; let (env1, skol_info2) = tidySkolemInfo env skol_info1
902 ; return (env1, GivenOrigin skol_info2) }
903 zonkTidyOrigin env (TypeEqOrigin { uo_actual = act, uo_expected = exp })
904 = do { (env1, act') <- zonkTidyTcType env act
905 ; (env2, exp') <- zonkTidyTcType env1 exp
906 ; return ( env2, TypeEqOrigin { uo_actual = act', uo_expected = exp' }) }
907 zonkTidyOrigin env (KindEqOrigin ty1 ty2 orig)
908 = do { (env1, ty1') <- zonkTidyTcType env ty1
909 ; (env2, ty2') <- zonkTidyTcType env1 ty2
910 ; (env3, orig') <- zonkTidyOrigin env2 orig
911 ; return (env3, KindEqOrigin ty1' ty2' orig') }
912 zonkTidyOrigin env (CoercibleOrigin ty1 ty2)
913 = do { (env1, ty1') <- zonkTidyTcType env ty1
914 ; (env2, ty2') <- zonkTidyTcType env1 ty2
915 ; return (env2, CoercibleOrigin ty1' ty2') }
916 zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
917 = do { (env1, p1') <- zonkTidyTcType env p1
918 ; (env2, p2') <- zonkTidyTcType env1 p2
919 ; return (env2, FunDepOrigin1 p1' l1 p2' l2) }
920 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
921 = do { (env1, p1') <- zonkTidyTcType env p1
922 ; (env2, p2') <- zonkTidyTcType env1 p2
923 ; (env3, o1') <- zonkTidyOrigin env2 o1
924 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
925 zonkTidyOrigin env orig = return (env, orig)
926
927 ----------------
928 tidyCt :: TidyEnv -> Ct -> Ct
929 -- Used only in error reporting
930 -- Also converts it to non-canonical
931 tidyCt env ct
932 = case ct of
933 CHoleCan { cc_ev = ev }
934 -> ct { cc_ev = tidy_ev env ev }
935 _ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
936 where
937 tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
938 -- NB: we do not tidy the ctev_evtm/var field because we don't
939 -- show it in error messages
940 tidy_ev env ctev@(CtGiven { ctev_pred = pred })
941 = ctev { ctev_pred = tidyType env pred }
942 tidy_ev env ctev@(CtWanted { ctev_pred = pred })
943 = ctev { ctev_pred = tidyType env pred }
944 tidy_ev env ctev@(CtDerived { ctev_pred = pred })
945 = ctev { ctev_pred = tidyType env pred }
946
947 ----------------
948 tidyEvVar :: TidyEnv -> EvVar -> EvVar
949 tidyEvVar env var = setVarType var (tidyType env (varType var))
950
951 ----------------
952 tidySkolemInfo :: TidyEnv -> SkolemInfo -> (TidyEnv, SkolemInfo)
953 tidySkolemInfo env (SigSkol cx ty)
954 = (env', SigSkol cx ty')
955 where
956 (env', ty') = tidyOpenType env ty
957
958 tidySkolemInfo env (InferSkol ids)
959 = (env', InferSkol ids')
960 where
961 (env', ids') = mapAccumL do_one env ids
962 do_one env (name, ty) = (env', (name, ty'))
963 where
964 (env', ty') = tidyOpenType env ty
965
966 tidySkolemInfo env (UnifyForAllSkol skol_tvs ty)
967 = (env1, UnifyForAllSkol skol_tvs' ty')
968 where
969 env1 = tidyFreeTyVars env (tyVarsOfType ty `delVarSetList` skol_tvs)
970 (env2, skol_tvs') = tidyTyVarBndrs env1 skol_tvs
971 ty' = tidyType env2 ty
972
973 tidySkolemInfo env info = (env, info)
974
975 {-
976 ************************************************************************
977 * *
978 (Named) Wildcards
979 * *
980 ************************************************************************
981 -}
982
983 -- | Create a new meta var with the given kind. This meta var should be used
984 -- to replace a wildcard in a type. Such a wildcard meta var can be
985 -- distinguished from other meta vars with the 'isWildcardVar' function.
986 newWildcardVar :: Name -> Kind -> TcM TcTyVar
987 newWildcardVar name kind = newNamedMetaTyVar name (TauTv True) kind
988
989 -- | Create a new meta var (which can unify with a type of any kind). This
990 -- meta var should be used to replace a wildcard in a type. Such a wildcard
991 -- meta var can be distinguished from other meta vars with the 'isWildcardVar'
992 -- function.
993 newWildcardVarMetaKind :: Name -> TcM TcTyVar
994 newWildcardVarMetaKind name = do kind <- newMetaKindVar
995 newWildcardVar name kind
996
997 -- | Return 'True' if the argument is a meta var created for a wildcard (by
998 -- 'newWildcardVar' or 'newWildcardVarMetaKind').
999 isWildcardVar :: TcTyVar -> Bool
1000 isWildcardVar tv | isTcTyVar tv, MetaTv (TauTv True) _ _ <- tcTyVarDetails tv = True
1001 isWildcardVar _ = False