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