Fix some substitution InScopeSets
[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, TupleSections, MultiWayIf #-}
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 newOpenFlexiTyVarTy,
23 newReturnTyVar, newReturnTyVarTy,
24 newOpenReturnTyVar,
25 newMetaKindVar, newMetaKindVars,
26 cloneMetaTyVar,
27 newFmvTyVar, newFskTyVar,
28 tauTvForReturnTv,
29
30 readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
31 newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
32
33 --------------------------------
34 -- Creating fresh type variables for pm checking
35 genInstSkolTyVarsX,
36
37 --------------------------------
38 -- Creating new evidence variables
39 newEvVar, newEvVars, newDict,
40 newWanted, newWanteds,
41 emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
42 newTcEvBinds, addTcEvBind,
43
44 newCoercionHole, fillCoercionHole, isFilledCoercionHole,
45 unpackCoercionHole, unpackCoercionHole_maybe,
46 checkCoercionHole,
47
48 --------------------------------
49 -- Instantiation
50 newMetaTyVars, newMetaTyVarX, newMetaSigTyVars,
51 newSigTyVar,
52 tcInstType,
53 tcInstSkolTyVars, tcInstSkolTyVarsLoc, tcInstSuperSkolTyVarsX,
54 tcInstSigTyVarsLoc, tcInstSigTyVars,
55 tcInstSkolType,
56 tcSkolDFunType, tcSuperSkolTyVars,
57
58 instSkolTyCoVars, freshenTyVarBndrs, freshenCoVarBndrsX,
59
60 --------------------------------
61 -- Zonking and tidying
62 zonkTidyTcType, zonkTidyOrigin,
63 mkTypeErrorThing, mkTypeErrorThingArgs,
64 tidyEvVar, tidyCt, tidySkolemInfo,
65 skolemiseUnboundMetaTyVar,
66 zonkTcTyVar, zonkTcTyVars, zonkTyCoVarsAndFV, zonkTcTypeAndFV,
67 zonkQuantifiedTyVar, zonkQuantifiedTyVarOrType, quantifyTyVars,
68 defaultKindVar,
69 zonkTcTyCoVarBndr, zonkTcType, zonkTcTypes, zonkCo,
70 zonkTyCoVarKind, zonkTcTypeMapper,
71
72 zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo,
73
74 tcGetGlobalTyCoVars
75 ) where
76
77 #include "HsVersions.h"
78
79 -- friends:
80 import TyCoRep ( CoercionHole(..) )
81 import TcType
82 import Type
83 import Coercion
84 import Class
85 import Var
86
87 -- others:
88 import TcRnMonad -- TcType, amongst others
89 import TcEvidence
90 import Id
91 import Name
92 import VarSet
93 import TysWiredIn
94 import TysPrim
95 import VarEnv
96 import PrelNames
97 import Util
98 import Outputable
99 import FastString
100 import SrcLoc
101 import Bag
102 import Pair
103 import qualified GHC.LanguageExtensions as LangExt
104
105 import Control.Monad
106 import Maybes
107 import Data.List ( mapAccumL, partition )
108
109 {-
110 ************************************************************************
111 * *
112 Kind variables
113 * *
114 ************************************************************************
115 -}
116
117 mkKindName :: Unique -> Name
118 mkKindName unique = mkSystemName unique kind_var_occ
119
120 kind_var_occ :: OccName -- Just one for all MetaKindVars
121 -- They may be jiggled by tidying
122 kind_var_occ = mkOccName tvName "k"
123
124 newMetaKindVar :: TcM TcKind
125 newMetaKindVar = do { uniq <- newUnique
126 ; details <- newMetaDetails TauTv
127 ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
128 ; return (mkTyVarTy kv) }
129
130 newMetaKindVars :: Int -> TcM [TcKind]
131 newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
132
133 {-
134 ************************************************************************
135 * *
136 Evidence variables; range over constraints we can abstract over
137 * *
138 ************************************************************************
139 -}
140
141 newEvVars :: TcThetaType -> TcM [EvVar]
142 newEvVars theta = mapM newEvVar theta
143
144 --------------
145
146 newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar
147 -- Creates new *rigid* variables for predicates
148 newEvVar ty = do { name <- newSysName (predTypeOccName ty)
149 ; return (mkLocalIdOrCoVar name ty) }
150
151 -- deals with both equality and non-equality predicates
152 newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
153 newWanted orig t_or_k pty
154 = do loc <- getCtLocM orig t_or_k
155 d <- if isEqPred pty then HoleDest <$> newCoercionHole
156 else EvVarDest <$> newEvVar pty
157 return $ CtWanted { ctev_dest = d
158 , ctev_pred = pty
159 , ctev_loc = loc }
160
161 newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
162 newWanteds orig = mapM (newWanted orig Nothing)
163
164 -- | Emits a new Wanted. Deals with both equalities and non-equalities.
165 emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
166 emitWanted origin pty
167 = do { ev <- newWanted origin Nothing pty
168 ; emitSimple $ mkNonCanonical ev
169 ; return $ ctEvTerm ev }
170
171 -- | Emits a new equality constraint
172 emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
173 emitWantedEq origin t_or_k role ty1 ty2
174 = do { hole <- newCoercionHole
175 ; loc <- getCtLocM origin (Just t_or_k)
176 ; emitSimple $ mkNonCanonical $
177 CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole, ctev_loc = loc }
178 ; return (mkHoleCo hole role ty1 ty2) }
179 where
180 pty = mkPrimEqPredRole role ty1 ty2
181
182 -- | Creates a new EvVar and immediately emits it as a Wanted.
183 -- No equality predicates here.
184 emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
185 emitWantedEvVar origin ty
186 = do { new_cv <- newEvVar ty
187 ; loc <- getCtLocM origin Nothing
188 ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
189 , ctev_pred = ty
190 , ctev_loc = loc }
191 ; emitSimple $ mkNonCanonical ctev
192 ; return new_cv }
193
194 emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
195 emitWantedEvVars orig = mapM (emitWantedEvVar orig)
196
197 newDict :: Class -> [TcType] -> TcM DictId
198 newDict cls tys
199 = do { name <- newSysName (mkDictOcc (getOccName cls))
200 ; return (mkLocalId name (mkClassPred cls tys)) }
201
202 predTypeOccName :: PredType -> OccName
203 predTypeOccName ty = case classifyPredType ty of
204 ClassPred cls _ -> mkDictOcc (getOccName cls)
205 EqPred _ _ _ -> mkVarOccFS (fsLit "cobox")
206 IrredPred _ -> mkVarOccFS (fsLit "irred")
207
208 {-
209 ************************************************************************
210 * *
211 Coercion holes
212 * *
213 ************************************************************************
214 -}
215
216 newCoercionHole :: TcM CoercionHole
217 newCoercionHole
218 = do { u <- newUnique
219 ; traceTc "New coercion hole:" (ppr u)
220 ; ref <- newMutVar Nothing
221 ; return $ CoercionHole u ref }
222
223 -- | Put a value in a coercion hole
224 fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
225 fillCoercionHole (CoercionHole u ref) co
226 = do {
227 #ifdef DEBUG
228 ; cts <- readTcRef ref
229 ; whenIsJust cts $ \old_co ->
230 pprPanic "Filling a filled coercion hole" (ppr u $$ ppr co $$ ppr old_co)
231 #endif
232 ; traceTc "Filling coercion hole" (ppr u <+> text ":=" <+> ppr co)
233 ; writeTcRef ref (Just co) }
234
235 -- | Is a coercion hole filled in?
236 isFilledCoercionHole :: CoercionHole -> TcM Bool
237 isFilledCoercionHole (CoercionHole _ ref) = isJust <$> readTcRef ref
238
239 -- | Retrieve the contents of a coercion hole. Panics if the hole
240 -- is unfilled
241 unpackCoercionHole :: CoercionHole -> TcM Coercion
242 unpackCoercionHole hole
243 = do { contents <- unpackCoercionHole_maybe hole
244 ; case contents of
245 Just co -> return co
246 Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) }
247
248 -- | Retrieve the contents of a coercion hole, if it is filled
249 unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
250 unpackCoercionHole_maybe (CoercionHole _ ref) = readTcRef ref
251
252 -- | Check that a coercion is appropriate for filling a hole. (The hole
253 -- itself is needed only for printing. NB: This must be /lazy/ in the coercion,
254 -- as it's used in TcHsSyn in the presence of knots.
255 -- Always returns the checked coercion, but this return value is necessary
256 -- so that the input coercion is forced only when the output is forced.
257 checkCoercionHole :: Coercion -> CoercionHole -> Role -> Type -> Type -> TcM Coercion
258 checkCoercionHole co h r t1 t2
259 -- co is already zonked, but t1 and t2 might not be
260 | debugIsOn
261 = do { t1 <- zonkTcType t1
262 ; t2 <- zonkTcType t2
263 ; let (Pair _t1 _t2, _role) = coercionKindRole co
264 ; return $
265 ASSERT2( t1 `eqType` _t1 && t2 `eqType` _t2 && r == _role
266 , (text "Bad coercion hole" <+>
267 ppr h <> colon <+> vcat [ ppr _t1, ppr _t2, ppr _role
268 , ppr co, ppr t1, ppr t2
269 , ppr r ]) )
270 co }
271 | otherwise
272 = return co
273
274
275 {-
276 ************************************************************************
277 * *
278 SkolemTvs (immutable)
279 * *
280 ************************************************************************
281 -}
282
283 tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
284 -- ^ How to instantiate the type variables
285 -> TcType -- ^ Type to instantiate
286 -> TcM ([TcTyVar], TcThetaType, TcType) -- ^ Result
287 -- (type vars, preds (incl equalities), rho)
288 tcInstType inst_tyvars ty
289 = case tcSplitForAllTys ty of
290 ([], rho) -> let -- There may be overloading despite no type variables;
291 -- (?x :: Int) => Int -> Int
292 (theta, tau) = tcSplitPhiTy rho
293 in
294 return ([], theta, tau)
295
296 (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
297 ; let (theta, tau) = tcSplitPhiTy (substTyUnchecked subst rho)
298 ; return (tyvars', theta, tau) }
299
300 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
301 -- Instantiate a type signature with skolem constants.
302 -- We could give them fresh names, but no need to do so
303 tcSkolDFunType ty = tcInstType tcInstSuperSkolTyVars ty
304
305 tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
306 -- Make skolem constants, but do *not* give them new names, as above
307 -- Moreover, make them "super skolems"; see comments with superSkolemTv
308 -- see Note [Kind substitution when instantiating]
309 -- Precondition: tyvars should be ordered by scoping
310 tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
311
312 tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
313 tcSuperSkolTyVar subst tv
314 = (extendTCvSubst (extendTCvInScope subst new_tv) tv (mkTyVarTy new_tv)
315 , new_tv)
316 where
317 kind = substTyUnchecked subst (tyVarKind tv)
318 new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
319
320 -- Wrappers
321 -- we need to be able to do this from outside the TcM monad:
322 tcInstSkolTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
323 tcInstSkolTyVarsLoc loc = instSkolTyCoVars (mkTcSkolTyVar loc False)
324
325 tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
326 tcInstSkolTyVars = tcInstSkolTyVars' False emptyTCvSubst
327
328 tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
329 tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
330
331 tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
332 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
333
334 tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
335 -- Precondition: tyvars should be ordered (kind vars first)
336 -- see Note [Kind substitution when instantiating]
337 -- Get the location from the monad; this is a complete freshening operation
338 tcInstSkolTyVars' overlappable subst tvs
339 = do { loc <- getSrcSpanM
340 ; instSkolTyCoVarsX (mkTcSkolTyVar loc overlappable) subst tvs }
341
342 mkTcSkolTyVar :: SrcSpan -> Bool -> Unique -> Name -> Kind -> TcTyVar
343 mkTcSkolTyVar loc overlappable uniq old_name kind
344 = mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
345 kind
346 (SkolemTv overlappable)
347
348 tcInstSigTyVarsLoc :: SrcSpan -> [TyVar]
349 -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
350 -- We specify the location
351 tcInstSigTyVarsLoc loc = instSkolTyCoVars (mkTcSkolTyVar loc False)
352
353 tcInstSigTyVars :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
354 -- Get the location from the TyVar itself, not the monad
355 tcInstSigTyVars
356 = instSkolTyCoVars mk_tv
357 where
358 mk_tv uniq old_name kind
359 = mkTcTyVar (setNameUnique old_name uniq) kind (SkolemTv False)
360
361 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
362 -- Instantiate a type with fresh skolem constants
363 -- Binding location comes from the monad
364 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
365
366 ------------------
367 freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
368 -- ^ Give fresh uniques to a bunch of TyVars, but they stay
369 -- as TyVars, rather than becoming TcTyVars
370 -- Used in FamInst.newFamInst, and Inst.newClsInst
371 freshenTyVarBndrs = instSkolTyCoVars mk_tv
372 where
373 mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
374
375 freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcRnIf gbl lcl (TCvSubst, [CoVar])
376 -- ^ Give fresh uniques to a bunch of CoVars
377 -- Used in FamInst.newFamInst
378 freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
379 where
380 mk_cv uniq old_name kind = mkCoVar (setNameUnique old_name uniq) kind
381
382 ------------------
383 instSkolTyCoVars :: (Unique -> Name -> Kind -> TyCoVar)
384 -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
385 instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
386
387 instSkolTyCoVarsX :: (Unique -> Name -> Kind -> TyCoVar)
388 -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
389 instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
390
391 instSkolTyCoVarX :: (Unique -> Name -> Kind -> TyCoVar)
392 -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
393 instSkolTyCoVarX mk_tcv subst tycovar
394 = do { uniq <- newUnique
395 ; let new_tv = mk_tcv uniq old_name kind
396 ; return (extendTCvSubst (extendTCvInScope subst new_tv) tycovar
397 (mk_ty_co new_tv)
398 , new_tv)
399 }
400 where
401 old_name = tyVarName tycovar
402 kind = substTyUnchecked subst (tyVarKind tycovar)
403
404 mk_ty_co v
405 | isTyVar v = mkTyVarTy v
406 | otherwise = mkCoercionTy $ mkCoVarCo v
407
408 newFskTyVar :: TcType -> TcM TcTyVar
409 newFskTyVar fam_ty
410 = do { uniq <- newUnique
411 ; let name = mkSysTvName uniq (fsLit "fsk")
412 ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
413
414 {-
415 Note [Kind substitution when instantiating]
416 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
417 When we instantiate a bunch of kind and type variables, first we
418 expect them to be topologically sorted.
419 Then we have to instantiate the kind variables, build a substitution
420 from old variables to the new variables, then instantiate the type
421 variables substituting the original kind.
422
423 Exemple: If we want to instantiate
424 [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
425 we want
426 [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
427 instead of the buggous
428 [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
429
430
431 ************************************************************************
432 * *
433 MetaTvs (meta type variables; mutable)
434 * *
435 ************************************************************************
436 -}
437
438 mkMetaTyVarName :: Unique -> FastString -> Name
439 -- Makes a /System/ Name, which is eagerly eliminated by
440 -- the unifier; see TcUnify.nicer_to_update_tv1, and
441 -- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
442 mkMetaTyVarName uniq str = mkSysTvName uniq str
443
444 newSigTyVar :: Name -> Kind -> TcM TcTyVar
445 newSigTyVar name kind
446 = do { details <- newMetaDetails SigTv
447 ; return (mkTcTyVar name kind details) }
448
449 newFmvTyVar :: TcType -> TcM TcTyVar
450 -- Very like newMetaTyVar, except sets mtv_tclvl to one less
451 -- so that the fmv is untouchable.
452 newFmvTyVar fam_ty
453 = do { uniq <- newUnique
454 ; ref <- newMutVar Flexi
455 ; cur_lvl <- getTcLevel
456 ; let details = MetaTv { mtv_info = FlatMetaTv
457 , mtv_ref = ref
458 , mtv_tclvl = fmvTcLevel cur_lvl }
459 name = mkMetaTyVarName uniq (fsLit "s")
460 ; return (mkTcTyVar name (typeKind fam_ty) details) }
461
462 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
463 newMetaDetails info
464 = do { ref <- newMutVar Flexi
465 ; tclvl <- getTcLevel
466 ; return (MetaTv { mtv_info = info
467 , mtv_ref = ref
468 , mtv_tclvl = tclvl }) }
469
470 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
471 cloneMetaTyVar tv
472 = ASSERT( isTcTyVar tv )
473 do { uniq <- newUnique
474 ; ref <- newMutVar Flexi
475 ; let name' = setNameUnique (tyVarName tv) uniq
476 details' = case tcTyVarDetails tv of
477 details@(MetaTv {}) -> details { mtv_ref = ref }
478 _ -> pprPanic "cloneMetaTyVar" (ppr tv)
479 ; return (mkTcTyVar name' (tyVarKind tv) details') }
480
481 -- Works for both type and kind variables
482 readMetaTyVar :: TyVar -> TcM MetaDetails
483 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
484 readMutVar (metaTvRef tyvar)
485
486 isFilledMetaTyVar :: TyVar -> TcM Bool
487 -- True of a filled-in (Indirect) meta type variable
488 isFilledMetaTyVar tv
489 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
490 = do { details <- readMutVar ref
491 ; return (isIndirect details) }
492 | otherwise = return False
493
494 isUnfilledMetaTyVar :: TyVar -> TcM Bool
495 -- True of a un-filled-in (Flexi) meta type variable
496 isUnfilledMetaTyVar tv
497 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
498 = do { details <- readMutVar ref
499 ; return (isFlexi details) }
500 | otherwise = return False
501
502 --------------------
503 -- Works with both type and kind variables
504 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
505 -- Write into a currently-empty MetaTyVar
506
507 writeMetaTyVar tyvar ty
508 | not debugIsOn
509 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
510
511 -- Everything from here on only happens if DEBUG is on
512 | not (isTcTyVar tyvar)
513 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
514 return ()
515
516 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
517 = writeMetaTyVarRef tyvar ref ty
518
519 | otherwise
520 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
521 return ()
522
523 --------------------
524 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
525 -- Here the tyvar is for error checking only;
526 -- the ref cell must be for the same tyvar
527 writeMetaTyVarRef tyvar ref ty
528 | not debugIsOn
529 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
530 <+> text ":=" <+> ppr ty)
531 ; writeTcRef ref (Indirect ty) }
532
533 -- Everything from here on only happens if DEBUG is on
534 | otherwise
535 = do { meta_details <- readMutVar ref;
536 -- Zonk kinds to allow the error check to work
537 ; zonked_tv_kind <- zonkTcType tv_kind
538 ; zonked_ty_kind <- zonkTcType ty_kind
539
540 -- Check for double updates
541 ; ASSERT2( isFlexi meta_details,
542 hang (text "Double update of meta tyvar")
543 2 (ppr tyvar $$ ppr meta_details) )
544
545 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
546 ; writeMutVar ref (Indirect ty)
547 ; when ( not (isPredTy tv_kind)
548 -- Don't check kinds for updates to coercion variables
549 && not (zonked_ty_kind `tcEqKind` zonked_tv_kind))
550 $ WARN( True, hang (text "Ill-kinded update to meta tyvar")
551 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
552 <+> text ":="
553 <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) ) )
554 (return ()) }
555 where
556 tv_kind = tyVarKind tyvar
557 ty_kind = typeKind ty
558
559 {-
560 % Generating fresh variables for pattern match check
561 -}
562
563 -- UNINSTANTIATED VERSION OF tcInstSkolTyCoVars
564 genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar]
565 -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
566 -- Precondition: tyvars should be scoping-ordered
567 -- see Note [Kind substitution when instantiating]
568 -- Get the location from the monad; this is a complete freshening operation
569 genInstSkolTyVarsX loc subst tvs = instSkolTyCoVarsX (mkTcSkolTyVar loc False) subst tvs
570
571 {-
572 ************************************************************************
573 * *
574 MetaTvs: TauTvs
575 * *
576 ************************************************************************
577
578 Note [Sort-polymorphic tyvars accept foralls]
579 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
580 Here is a common paradigm:
581 foo :: (forall a. a -> a) -> Int
582 foo = error "urk"
583 To make this work we need to instantiate 'error' with a polytype.
584 A similar case is
585 bar :: Bool -> (forall a. a->a) -> Int
586 bar True = \x. (x 3)
587 bar False = error "urk"
588 Here we need to instantiate 'error' with a polytype.
589
590 But 'error' has an sort-polymorphic type variable, precisely so that
591 we can instantiate it with Int#. So we also allow such type variables
592 to be instantiate with foralls. It's a bit of a hack, but seems
593 straightforward.
594
595 Note [Never need to instantiate coercion variables]
596 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
597 With coercion variables sloshing around in types, it might seem that we
598 sometimes need to instantiate coercion variables. This would be problematic,
599 because coercion variables inhabit unboxed equality (~#), and the constraint
600 solver thinks in terms only of boxed equality (~). The solution is that
601 we never need to instantiate coercion variables in the first place.
602
603 The tyvars that we need to instantiate come from the types of functions,
604 data constructors, and patterns. These will never be quantified over
605 coercion variables, except for the special case of the promoted Eq#. But,
606 that can't ever appear in user code, so we're safe!
607 -}
608
609 newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
610 -- Make a new meta tyvar out of thin air
611 newAnonMetaTyVar meta_info kind
612 = do { uniq <- newUnique
613 ; let name = mkMetaTyVarName uniq s
614 s = case meta_info of
615 ReturnTv -> fsLit "r"
616 TauTv -> fsLit "t"
617 FlatMetaTv -> fsLit "fmv"
618 SigTv -> fsLit "a"
619 ; details <- newMetaDetails meta_info
620 ; return (mkTcTyVar name kind details) }
621
622 newFlexiTyVar :: Kind -> TcM TcTyVar
623 newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
624
625 newFlexiTyVarTy :: Kind -> TcM TcType
626 newFlexiTyVarTy kind = do
627 tc_tyvar <- newFlexiTyVar kind
628 return (mkTyVarTy tc_tyvar)
629
630 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
631 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
632
633 newReturnTyVar :: Kind -> TcM TcTyVar
634 newReturnTyVar kind = newAnonMetaTyVar ReturnTv kind
635
636 newReturnTyVarTy :: Kind -> TcM TcType
637 newReturnTyVarTy kind = mkTyVarTy <$> newReturnTyVar kind
638
639 -- | Create a tyvar that can be a lifted or unlifted type.
640 newOpenFlexiTyVarTy :: TcM TcType
641 newOpenFlexiTyVarTy
642 = do { lev <- newFlexiTyVarTy levityTy
643 ; newFlexiTyVarTy (tYPE lev) }
644
645 -- | Create a *return* tyvar that can be a lifted or unlifted type.
646 newOpenReturnTyVar :: TcM (TcTyVar, TcKind)
647 newOpenReturnTyVar
648 = do { lev <- newFlexiTyVarTy levityTy -- this doesn't need ReturnTv
649 ; let k = tYPE lev
650 ; tv <- newReturnTyVar k
651 ; return (tv, k) }
652
653 -- | If the type is a ReturnTv, fill it with a new meta-TauTv. Otherwise,
654 -- no change. This function can look through ReturnTvs and returns a partially
655 -- zonked type as an optimisation.
656 tauTvForReturnTv :: TcType -> TcM TcType
657 tauTvForReturnTv ty
658 | Just tv <- tcGetTyVar_maybe ty
659 , isReturnTyVar tv
660 = do { contents <- readMetaTyVar tv
661 ; case contents of
662 Flexi -> do { tau_ty <- newFlexiTyVarTy (tyVarKind tv)
663 ; writeMetaTyVar tv tau_ty
664 ; return tau_ty }
665 Indirect ty -> tauTvForReturnTv ty }
666 | otherwise
667 = ASSERT( all (not . isReturnTyVar) (tyCoVarsOfTypeList ty) )
668 return ty
669
670 newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
671 newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
672
673 newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
674 -- Instantiate with META type variables
675 -- Note that this works for a sequence of kind, type, and coercion variables
676 -- variables. Eg [ (k:*), (a:k->k) ]
677 -- Gives [ (k7:*), (a8:k7->k7) ]
678 newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
679 -- emptyTCvSubst has an empty in-scope set, but that's fine here
680 -- Since the tyvars are freshly made, they cannot possibly be
681 -- captured by any existing for-alls.
682
683 newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
684 -- Make a new unification variable tyvar whose Name and Kind come from
685 -- an existing TyVar. We substitute kind variables in the kind.
686 newMetaTyVarX subst tyvar
687 = do { uniq <- newUnique
688 -- See Note [Levity polymorphic variables accept foralls]
689 ; let info | isLevityPolymorphic (tyVarKind tyvar) = ReturnTv
690 | otherwise = TauTv
691 ; details <- newMetaDetails info
692 ; let name = mkSystemName uniq (getOccName tyvar)
693 -- See Note [Name of an instantiated type variable]
694 kind = substTyUnchecked subst (tyVarKind tyvar)
695 new_tv = mkTcTyVar name kind details
696 ; return (extendTCvSubstAndInScope subst tyvar
697 (mkTyVarTy new_tv)
698 , new_tv)
699 }
700
701 newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
702 -- Just like newMetaTyVarX, but make a SigTv
703 newMetaSigTyVarX subst tyvar
704 = do { uniq <- newUnique
705 ; details <- newMetaDetails SigTv
706 ; let name = mkSystemName uniq (getOccName tyvar)
707 kind = substTy subst (tyVarKind tyvar)
708 new_tv = mkTcTyVar name kind details
709 ; return (extendTCvSubst (extendTCvInScope subst new_tv) tyvar
710 (mkTyVarTy new_tv)
711 , new_tv) }
712
713 {- Note [Name of an instantiated type variable]
714 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
715 At the moment we give a unification variable a System Name, which
716 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
717
718 Note [Levity polymorphic variables accept foralls]
719 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
720 Here is a common paradigm:
721 foo :: (forall a. a -> a) -> Int
722 foo = error "urk"
723 To make this work we need to instantiate 'error' with a polytype.
724 A similar case is
725 bar :: Bool -> (forall a. a->a) -> Int
726 bar True = \x. (x 3)
727 bar False = error "urk"
728 Here we need to instantiate 'error' with a polytype.
729
730 But 'error' has a levity polymorphic type variable, precisely so that
731 we can instantiate it with Int#. So we also allow such type variables
732 to be instantiated with foralls. It's a bit of a hack, but seems
733 straightforward.
734
735 ************************************************************************
736 * *
737 Quantification
738 * *
739 ************************************************************************
740
741 Note [quantifyTyVars]
742 ~~~~~~~~~~~~~~~~~~~~~
743 quantifyTyVars is given the free vars of a type that we
744 are about to wrap in a forall.
745
746 It takes these free type/kind variables (partitioned into dependent and
747 non-dependent variables) and
748 1. Zonks them and remove globals and covars
749 2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
750 3. Calls zonkQuantifiedTyVar on each
751
752 Step (2) is often unimportant, because the kind variable is often
753 also free in the type. Eg
754 Typeable k (a::k)
755 has free vars {k,a}. But the type (see Trac #7916)
756 (f::k->*) (a::k)
757 has free vars {f,a}, but we must add 'k' as well! Hence step (3).
758
759 This function bothers to distinguish between dependent and non-dependent
760 variables only to keep correct defaulting behavior with -XNoPolyKinds.
761 With -XPolyKinds, it treats both classes of variables identically.
762
763 Note that this function can accept covars, but will never return them.
764 This is because we never want to infer a quantified covar!
765 -}
766
767 quantifyTyVars :: TcTyCoVarSet -- global tvs
768 -> Pair TcTyCoVarSet -- dependent tvs We only distinguish
769 -- nondependent tvs between these for
770 -- -XNoPolyKinds
771 -> TcM [TcTyVar]
772 -- See Note [quantifyTyVars]
773 -- Can be given a mixture of TcTyVars and TyVars, in the case of
774 -- associated type declarations. Also accepts covars, but *never* returns any.
775
776 quantifyTyVars gbl_tvs (Pair dep_tkvs nondep_tkvs)
777 = do { dep_tkvs <- zonkTyCoVarsAndFV dep_tkvs
778 ; nondep_tkvs <- (`minusVarSet` dep_tkvs) <$>
779 zonkTyCoVarsAndFV nondep_tkvs
780 ; gbl_tvs <- zonkTyCoVarsAndFV gbl_tvs
781
782 ; let all_cvs = filterVarSet isCoVar $
783 dep_tkvs `unionVarSet` nondep_tkvs `minusVarSet` gbl_tvs
784 dep_kvs = varSetElemsWellScoped $
785 dep_tkvs `minusVarSet` gbl_tvs
786 `minusVarSet` (closeOverKinds all_cvs)
787 -- remove any tvs that a covar depends on
788
789 nondep_tvs = varSetElemsWellScoped $
790 nondep_tkvs `minusVarSet` gbl_tvs
791 -- no worry about dependent cvs here, as these vars
792 -- are non-dependent
793
794 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
795
796 -- In the non-PolyKinds case, default the kind variables
797 -- to *, and zonk the tyvars as usual. Notice that this
798 -- may make quantifyTyVars return a shorter list
799 -- than it was passed, but that's ok
800 ; poly_kinds <- xoptM LangExt.PolyKinds
801 ; dep_vars2 <- if poly_kinds
802 then return dep_kvs
803 else do { let (meta_kvs, skolem_kvs) = partition is_meta dep_kvs
804 is_meta kv = isTcTyVar kv && isMetaTyVar kv
805
806 ; mapM_ defaultKindVar meta_kvs
807 ; return skolem_kvs } -- should be empty
808
809 ; let quant_vars = dep_vars2 ++ nondep_tvs
810
811 ; traceTc "quantifyTyVars"
812 (vcat [ text "globals:" <+> ppr gbl_tvs
813 , text "nondep:" <+> ppr nondep_tvs
814 , text "dep:" <+> ppr dep_kvs
815 , text "dep2:" <+> ppr dep_vars2
816 , text "quant_vars:" <+> ppr quant_vars ])
817
818 ; mapMaybeM zonk_quant quant_vars }
819 -- Because of the order, any kind variables
820 -- mentioned in the kinds of the type variables refer to
821 -- the now-quantified versions
822 where
823 zonk_quant tkv
824 | isTcTyVar tkv = zonkQuantifiedTyVar tkv
825 | otherwise = return $ Just tkv
826 -- For associated types, we have the class variables
827 -- in scope, and they are TyVars not TcTyVars
828
829 zonkQuantifiedTyVar :: TcTyVar -> TcM (Maybe TcTyVar)
830 -- The quantified type variables often include meta type variables
831 -- we want to freeze them into ordinary type variables, and
832 -- default their kind (e.g. from TYPE v to TYPE Lifted)
833 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
834 -- bound occurrences of the original type variable will get zonked to
835 -- the immutable version.
836 --
837 -- We leave skolem TyVars alone; they are immutable.
838 --
839 -- This function is called on both kind and type variables,
840 -- but kind variables *only* if PolyKinds is on.
841 --
842 -- This returns a tyvar if it should be quantified over; otherwise,
843 -- it returns Nothing. Nothing is
844 -- returned only if zonkQuantifiedTyVar is passed a Levity meta-tyvar,
845 -- in order to default to Lifted.
846 zonkQuantifiedTyVar tv = left_only `liftM` zonkQuantifiedTyVarOrType tv
847 where left_only :: Either a b -> Maybe a
848 left_only (Left x) = Just x
849 left_only (Right _) = Nothing
850
851 -- | Like zonkQuantifiedTyVar, but if zonking reveals that the tyvar
852 -- should become a type (when defaulting a levity var to Lifted), it
853 -- returns the type instead.
854 zonkQuantifiedTyVarOrType :: TcTyVar -> TcM (Either TcTyVar TcType)
855 zonkQuantifiedTyVarOrType tv
856 = case tcTyVarDetails tv of
857 SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
858 ; return $ Left $ setTyVarKind tv kind }
859 -- It might be a skolem type variable,
860 -- for example from a user type signature
861
862 MetaTv { mtv_ref = ref } ->
863 do when debugIsOn $ do
864 -- [Sept 04] Check for non-empty.
865 -- See note [Silly Type Synonym]
866 cts <- readMutVar ref
867 case cts of
868 Flexi -> return ()
869 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
870 return ()
871 if isLevityVar tv
872 then do { writeMetaTyVar tv liftedDataConTy
873 ; return (Right liftedDataConTy) }
874 else Left `liftM` skolemiseUnboundMetaTyVar tv vanillaSkolemTv
875 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
876
877 -- | Take an (unconstrained) meta tyvar and default it. Works only for
878 -- kind vars (of type BOX) and levity vars (of type Levity).
879 defaultKindVar :: TcTyVar -> TcM Kind
880 defaultKindVar kv
881 | ASSERT( isMetaTyVar kv )
882 isLevityVar kv
883 = writeMetaTyVar kv liftedDataConTy >> return liftedDataConTy
884 | otherwise
885 = writeMetaTyVar kv liftedTypeKind >> return liftedTypeKind
886
887 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
888 -- We have a Meta tyvar with a ref-cell inside it
889 -- Skolemise it, so that
890 -- we are totally out of Meta-tyvar-land
891 -- We create a skolem TyVar, not a regular TyVar
892 -- See Note [Zonking to Skolem]
893 skolemiseUnboundMetaTyVar tv details
894 = ASSERT2( isMetaTyVar tv, ppr tv )
895 do { span <- getSrcSpanM -- Get the location from "here"
896 -- ie where we are generalising
897 ; kind <- zonkTcType (tyVarKind tv)
898 ; let uniq = getUnique tv
899 -- NB: Use same Unique as original tyvar. This is
900 -- important for TcHsType.splitTelescopeTvs to work properly
901
902 tv_name = getOccName tv
903 final_name = mkInternalName uniq tv_name span
904 final_tv = mkTcTyVar final_name kind details
905
906 ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
907 ; writeMetaTyVar tv (mkTyVarTy final_tv)
908 ; return final_tv }
909
910 {-
911 Note [Zonking to Skolem]
912 ~~~~~~~~~~~~~~~~~~~~~~~~
913 We used to zonk quantified type variables to regular TyVars. However, this
914 leads to problems. Consider this program from the regression test suite:
915
916 eval :: Int -> String -> String -> String
917 eval 0 root actual = evalRHS 0 root actual
918
919 evalRHS :: Int -> a
920 evalRHS 0 root actual = eval 0 root actual
921
922 It leads to the deferral of an equality (wrapped in an implication constraint)
923
924 forall a. () => ((String -> String -> String) ~ a)
925
926 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
927 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
928 This has the *side effect* of also zonking the `a' in the deferred equality
929 (which at this point is being handed around wrapped in an implication
930 constraint).
931
932 Finally, the equality (with the zonked `a') will be handed back to the
933 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
934 If we zonk `a' with a regular type variable, we will have this regular type
935 variable now floating around in the simplifier, which in many places assumes to
936 only see proper TcTyVars.
937
938 We can avoid this problem by zonking with a skolem. The skolem is rigid
939 (which we require for a quantified variable), but is still a TcTyVar that the
940 simplifier knows how to deal with.
941
942 Note [Silly Type Synonyms]
943 ~~~~~~~~~~~~~~~~~~~~~~~~~~
944 Consider this:
945 type C u a = u -- Note 'a' unused
946
947 foo :: (forall a. C u a -> C u a) -> u
948 foo x = ...
949
950 bar :: Num u => u
951 bar = foo (\t -> t + t)
952
953 * From the (\t -> t+t) we get type {Num d} => d -> d
954 where d is fresh.
955
956 * Now unify with type of foo's arg, and we get:
957 {Num (C d a)} => C d a -> C d a
958 where a is fresh.
959
960 * Now abstract over the 'a', but float out the Num (C d a) constraint
961 because it does not 'really' mention a. (see exactTyVarsOfType)
962 The arg to foo becomes
963 \/\a -> \t -> t+t
964
965 * So we get a dict binding for Num (C d a), which is zonked to give
966 a = ()
967 [Note Sept 04: now that we are zonking quantified type variables
968 on construction, the 'a' will be frozen as a regular tyvar on
969 quantification, so the floated dict will still have type (C d a).
970 Which renders this whole note moot; happily!]
971
972 * Then the \/\a abstraction has a zonked 'a' in it.
973
974 All very silly. I think its harmless to ignore the problem. We'll end up with
975 a \/\a in the final result but all the occurrences of a will be zonked to ()
976
977 ************************************************************************
978 * *
979 Zonking types
980 * *
981 ************************************************************************
982
983 -}
984
985 -- | @tcGetGlobalTyCoVars@ returns a fully-zonked set of *scoped* tyvars free in
986 -- the environment. To improve subsequent calls to the same function it writes
987 -- the zonked set back into the environment. Note that this returns all
988 -- variables free in anything (term-level or type-level) in scope. We thus
989 -- don't have to worry about clashes with things that are not in scope, because
990 -- if they are reachable, then they'll be returned here.
991 tcGetGlobalTyCoVars :: TcM TcTyVarSet
992 tcGetGlobalTyCoVars
993 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
994 ; gbl_tvs <- readMutVar gtv_var
995 ; gbl_tvs' <- zonkTyCoVarsAndFV gbl_tvs
996 ; writeMutVar gtv_var gbl_tvs'
997 ; return gbl_tvs' }
998
999 zonkTcTypeAndFV :: TcType -> TcM TyCoVarSet
1000 -- Zonk a type and take its free variables
1001 -- With kind polymorphism it can be essential to zonk *first*
1002 -- so that we find the right set of free variables. Eg
1003 -- forall k1. forall (a:k2). a
1004 -- where k2:=k1 is in the substitution. We don't want
1005 -- k2 to look free in this type!
1006 -- NB: This might be called from within the knot, so don't use
1007 -- smart constructors. See Note [Zonking within the knot] in TcHsType
1008 zonkTcTypeAndFV ty
1009 = tyCoVarsOfType <$> mapType (zonkTcTypeMapper { tcm_smart = False }) () ty
1010
1011 zonkTyCoVar :: TyCoVar -> TcM TcType
1012 -- Works on TyVars and TcTyVars
1013 zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
1014 | isTyVar tv = mkTyVarTy <$> zonkTyCoVarKind tv
1015 | otherwise = ASSERT2( isCoVar tv, ppr tv )
1016 mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
1017 -- Hackily, when typechecking type and class decls
1018 -- we have TyVars in scopeadded (only) in
1019 -- TcHsType.tcTyClTyVars, but it seems
1020 -- painful to make them into TcTyVars there
1021
1022 zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
1023 zonkTyCoVarsAndFV tycovars = tyCoVarsOfTypes <$> mapM zonkTyCoVar (varSetElems tycovars)
1024
1025 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
1026 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
1027
1028 ----------------- Types
1029 zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
1030 zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
1031 ; return (setTyVarKind tv kind') }
1032
1033 zonkTcTypes :: [TcType] -> TcM [TcType]
1034 zonkTcTypes tys = mapM zonkTcType tys
1035
1036 {-
1037 ************************************************************************
1038 * *
1039 Zonking constraints
1040 * *
1041 ************************************************************************
1042 -}
1043
1044 zonkImplication :: Implication -> TcM Implication
1045 zonkImplication implic@(Implic { ic_skols = skols
1046 , ic_given = given
1047 , ic_wanted = wanted
1048 , ic_info = info })
1049 = do { skols' <- mapM zonkTcTyCoVarBndr skols -- Need to zonk their kinds!
1050 -- as Trac #7230 showed
1051 ; given' <- mapM zonkEvVar given
1052 ; info' <- zonkSkolemInfo info
1053 ; wanted' <- zonkWCRec wanted
1054 ; return (implic { ic_skols = skols'
1055 , ic_given = given'
1056 , ic_wanted = wanted'
1057 , ic_info = info' }) }
1058
1059 zonkEvVar :: EvVar -> TcM EvVar
1060 zonkEvVar var = do { ty' <- zonkTcType (varType var)
1061 ; return (setVarType var ty') }
1062
1063
1064 zonkWC :: WantedConstraints -> TcM WantedConstraints
1065 zonkWC wc = zonkWCRec wc
1066
1067 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
1068 zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
1069 = do { simple' <- zonkSimples simple
1070 ; implic' <- mapBagM zonkImplication implic
1071 ; insol' <- zonkSimples insol
1072 ; return (WC { wc_simple = simple', wc_impl = implic', wc_insol = insol' }) }
1073
1074 zonkSimples :: Cts -> TcM Cts
1075 zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
1076 ; traceTc "zonkSimples done:" (ppr cts')
1077 ; return cts' }
1078
1079 zonkCt' :: Ct -> TcM Ct
1080 zonkCt' ct = zonkCt ct
1081
1082 zonkCt :: Ct -> TcM Ct
1083 zonkCt ct@(CHoleCan { cc_ev = ev })
1084 = do { ev' <- zonkCtEvidence ev
1085 ; return $ ct { cc_ev = ev' } }
1086 zonkCt ct
1087 = do { fl' <- zonkCtEvidence (cc_ev ct)
1088 ; return (mkNonCanonical fl') }
1089
1090 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
1091 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
1092 = do { pred' <- zonkTcType pred
1093 ; return (ctev { ctev_pred = pred'}) }
1094 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest })
1095 = do { pred' <- zonkTcType pred
1096 ; let dest' = case dest of
1097 EvVarDest ev -> EvVarDest $ setVarType ev pred'
1098 -- necessary in simplifyInfer
1099 HoleDest h -> HoleDest h
1100 ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
1101 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
1102 = do { pred' <- zonkTcType pred
1103 ; return (ctev { ctev_pred = pred' }) }
1104
1105 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
1106 zonkSkolemInfo (SigSkol cx ty) = do { ty' <- zonkTcType ty
1107 ; return (SigSkol cx ty') }
1108 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
1109 ; return (InferSkol ntys') }
1110 where
1111 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
1112 zonkSkolemInfo skol_info = return skol_info
1113
1114 {-
1115 %************************************************************************
1116 %* *
1117 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
1118 * *
1119 * For internal use only! *
1120 * *
1121 ************************************************************************
1122
1123 -}
1124
1125 -- zonkId is used *during* typechecking just to zonk the Id's type
1126 zonkId :: TcId -> TcM TcId
1127 zonkId id
1128 = do { ty' <- zonkTcType (idType id)
1129 ; return (Id.setIdType id ty') }
1130
1131 -- | A suitable TyCoMapper for zonking a type inside the knot, and
1132 -- before all metavars are filled in.
1133 zonkTcTypeMapper :: TyCoMapper () TcM
1134 zonkTcTypeMapper = TyCoMapper
1135 { tcm_smart = True
1136 , tcm_tyvar = const zonkTcTyVar
1137 , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
1138 , tcm_hole = hole
1139 , tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv }
1140 where
1141 hole :: () -> CoercionHole -> Role -> Type -> Type
1142 -> TcM Coercion
1143 hole _ h r t1 t2
1144 = do { contents <- unpackCoercionHole_maybe h
1145 ; case contents of
1146 Just co -> do { co <- zonkCo co
1147 ; checkCoercionHole co h r t1 t2 }
1148 Nothing -> do { t1 <- zonkTcType t1
1149 ; t2 <- zonkTcType t2
1150 ; return $ mkHoleCo h r t1 t2 } }
1151
1152
1153 -- For unbound, mutable tyvars, zonkType uses the function given to it
1154 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
1155 -- type variable and zonks the kind too
1156 zonkTcType :: TcType -> TcM TcType
1157 zonkTcType = mapType zonkTcTypeMapper ()
1158
1159 -- | "Zonk" a coercion -- really, just zonk any types in the coercion
1160 zonkCo :: Coercion -> TcM Coercion
1161 zonkCo = mapCoercion zonkTcTypeMapper ()
1162
1163 zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
1164 -- A tyvar binder is never a unification variable (MetaTv),
1165 -- rather it is always a skolems. BUT it may have a kind
1166 -- that has not yet been zonked, and may include kind
1167 -- unification variables.
1168 zonkTcTyCoVarBndr tyvar
1169 -- can't use isCoVar, because it looks at a TyCon. Argh.
1170 = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), ppr tyvar ) do
1171 updateTyVarKindM zonkTcType tyvar
1172
1173 zonkTcTyVar :: TcTyVar -> TcM TcType
1174 -- Simply look through all Flexis
1175 zonkTcTyVar tv
1176 | isTcTyVar tv
1177 = case tcTyVarDetails tv of
1178 SkolemTv {} -> zonk_kind_and_return
1179 RuntimeUnk {} -> zonk_kind_and_return
1180 FlatSkol ty -> zonkTcType ty
1181 MetaTv { mtv_ref = ref }
1182 -> do { cts <- readMutVar ref
1183 ; case cts of
1184 Flexi -> zonk_kind_and_return
1185 Indirect ty -> zonkTcType ty }
1186
1187 | otherwise -- coercion variable
1188 = zonk_kind_and_return
1189 where
1190 zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv
1191 ; return (mkTyVarTy z_tv) }
1192
1193 {-
1194 %************************************************************************
1195 %* *
1196 Tidying
1197 * *
1198 ************************************************************************
1199 -}
1200
1201 zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
1202 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
1203 ; return (tidyOpenType env ty') }
1204
1205 -- | Make an 'ErrorThing' storing a type.
1206 mkTypeErrorThing :: TcType -> ErrorThing
1207 mkTypeErrorThing ty = ErrorThing ty (Just $ length $ snd $ splitAppTys ty)
1208 zonkTidyTcType
1209
1210 -- | Make an 'ErrorThing' storing a type, with some extra args known about
1211 mkTypeErrorThingArgs :: TcType -> Int -> ErrorThing
1212 mkTypeErrorThingArgs ty num_args
1213 = ErrorThing ty (Just $ (length $ snd $ splitAppTys ty) + num_args)
1214 zonkTidyTcType
1215
1216 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
1217 zonkTidyOrigin env (GivenOrigin skol_info)
1218 = do { skol_info1 <- zonkSkolemInfo skol_info
1219 ; let skol_info2 = tidySkolemInfo env skol_info1
1220 ; return (env, GivenOrigin skol_info2) }
1221 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act
1222 , uo_expected = exp
1223 , uo_thing = m_thing })
1224 = do { (env1, act') <- zonkTidyTcType env act
1225 ; (env2, exp') <- zonkTidyTcType env1 exp
1226 ; (env3, m_thing') <- zonkTidyErrorThing env2 m_thing
1227 ; return ( env3, orig { uo_actual = act'
1228 , uo_expected = exp'
1229 , uo_thing = m_thing' }) }
1230 zonkTidyOrigin env (KindEqOrigin ty1 ty2 orig t_or_k)
1231 = do { (env1, ty1') <- zonkTidyTcType env ty1
1232 ; (env2, ty2') <- zonkTidyTcType env1 ty2
1233 ; (env3, orig') <- zonkTidyOrigin env2 orig
1234 ; return (env3, KindEqOrigin ty1' ty2' orig' t_or_k) }
1235 zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
1236 = do { (env1, p1') <- zonkTidyTcType env p1
1237 ; (env2, p2') <- zonkTidyTcType env1 p2
1238 ; return (env2, FunDepOrigin1 p1' l1 p2' l2) }
1239 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
1240 = do { (env1, p1') <- zonkTidyTcType env p1
1241 ; (env2, p2') <- zonkTidyTcType env1 p2
1242 ; (env3, o1') <- zonkTidyOrigin env2 o1
1243 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
1244 zonkTidyOrigin env orig = return (env, orig)
1245
1246 zonkTidyErrorThing :: TidyEnv -> Maybe ErrorThing
1247 -> TcM (TidyEnv, Maybe ErrorThing)
1248 zonkTidyErrorThing env (Just (ErrorThing thing n_args zonker))
1249 = do { (env', thing') <- zonker env thing
1250 ; return (env', Just $ ErrorThing thing' n_args zonker) }
1251 zonkTidyErrorThing env Nothing
1252 = return (env, Nothing)
1253
1254 ----------------
1255 tidyCt :: TidyEnv -> Ct -> Ct
1256 -- Used only in error reporting
1257 -- Also converts it to non-canonical
1258 tidyCt env ct
1259 = case ct of
1260 CHoleCan { cc_ev = ev }
1261 -> ct { cc_ev = tidy_ev env ev }
1262 _ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
1263 where
1264 tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
1265 -- NB: we do not tidy the ctev_evar field because we don't
1266 -- show it in error messages
1267 tidy_ev env ctev@(CtGiven { ctev_pred = pred })
1268 = ctev { ctev_pred = tidyType env pred }
1269 tidy_ev env ctev@(CtWanted { ctev_pred = pred })
1270 = ctev { ctev_pred = tidyType env pred }
1271 tidy_ev env ctev@(CtDerived { ctev_pred = pred })
1272 = ctev { ctev_pred = tidyType env pred }
1273
1274 ----------------
1275 tidyEvVar :: TidyEnv -> EvVar -> EvVar
1276 tidyEvVar env var = setVarType var (tidyType env (varType var))
1277
1278 ----------------
1279 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
1280 tidySkolemInfo env (DerivSkol ty) = DerivSkol (tidyType env ty)
1281 tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (tidyType env ty)
1282 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
1283 tidySkolemInfo env (UnifyForAllSkol ty) = UnifyForAllSkol (tidyType env ty)
1284 tidySkolemInfo _ info = info