Change "cobox" to "co" in debug output
[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, newOpenTypeKind,
23 newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel,
24 cloneMetaTyVar,
25 newFmvTyVar, newFskTyVar,
26
27 readMetaTyVar, writeMetaTyVar,
28 newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
29
30 --------------------------------
31 -- Expected types
32 ExpType(..), ExpSigmaType, ExpRhoType,
33 mkCheckExpType,
34 newInferExpType, newInferExpTypeInst, newInferExpTypeNoInst,
35 readExpType, readExpType_maybe,
36 expTypeToType, checkingExpType_maybe, checkingExpType,
37 tauifyExpType, inferResultToType,
38
39 --------------------------------
40 -- Creating fresh type variables for pm checking
41 genInstSkolTyVarsX,
42
43 --------------------------------
44 -- Creating new evidence variables
45 newEvVar, newEvVars, newDict,
46 newWanted, newWanteds, cloneWanted, cloneWC,
47 emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
48 newTcEvBinds, addTcEvBind,
49
50 newCoercionHole, fillCoercionHole, isFilledCoercionHole,
51 unpackCoercionHole, unpackCoercionHole_maybe,
52 checkCoercionHole,
53
54 --------------------------------
55 -- Instantiation
56 newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
57 newMetaSigTyVars, newMetaSigTyVarX,
58 newSigTyVar, newWildCardX,
59 tcInstType,
60 tcInstSkolTyVars,tcInstSkolTyVarsX,
61 tcInstSuperSkolTyVarsX,
62 tcSkolDFunType, tcSuperSkolTyVars,
63
64 instSkolTyCoVars, freshenTyVarBndrs, freshenCoVarBndrsX,
65
66 --------------------------------
67 -- Zonking and tidying
68 zonkTidyTcType, zonkTidyOrigin,
69 tidyEvVar, tidyCt, tidySkolemInfo,
70 skolemiseRuntimeUnk,
71 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarToTyVar,
72 zonkTyCoVarsAndFV, zonkTcTypeAndFV,
73 zonkTyCoVarsAndFVList,
74 zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
75 zonkQuantifiedTyVar, defaultTyVar,
76 quantifyTyVars,
77 zonkTcTyCoVarBndr, zonkTcTyVarBinder,
78 zonkTcType, zonkTcTypes, zonkCo,
79 zonkTyCoVarKind, zonkTcTypeMapper,
80
81 zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo,
82
83 tcGetGlobalTyCoVars,
84
85 ------------------------------
86 -- Levity polymorphism
87 ensureNotLevPoly, checkForLevPoly, checkForLevPolyX, formatLevPolyErr
88 ) where
89
90 #include "HsVersions.h"
91
92 -- friends:
93 import GhcPrelude
94
95 import TyCoRep
96 import TcType
97 import Type
98 import Kind
99 import Coercion
100 import Class
101 import Var
102
103 -- others:
104 import TcRnMonad -- TcType, amongst others
105 import TcEvidence
106 import Id
107 import Name
108 import VarSet
109 import TysWiredIn
110 import TysPrim
111 import VarEnv
112 import NameEnv
113 import PrelNames
114 import Util
115 import Outputable
116 import FastString
117 import SrcLoc
118 import Bag
119 import Pair
120 import UniqSet
121 import qualified GHC.LanguageExtensions as LangExt
122
123 import Control.Monad
124 import Maybes
125 import Data.List ( mapAccumL )
126 import Control.Arrow ( second )
127
128 {-
129 ************************************************************************
130 * *
131 Kind variables
132 * *
133 ************************************************************************
134 -}
135
136 mkKindName :: Unique -> Name
137 mkKindName unique = mkSystemName unique kind_var_occ
138
139 kind_var_occ :: OccName -- Just one for all MetaKindVars
140 -- They may be jiggled by tidying
141 kind_var_occ = mkOccName tvName "k"
142
143 newMetaKindVar :: TcM TcKind
144 newMetaKindVar = do { uniq <- newUnique
145 ; details <- newMetaDetails TauTv
146 ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
147 ; return (mkTyVarTy kv) }
148
149 newMetaKindVars :: Int -> TcM [TcKind]
150 newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
151
152 {-
153 ************************************************************************
154 * *
155 Evidence variables; range over constraints we can abstract over
156 * *
157 ************************************************************************
158 -}
159
160 newEvVars :: TcThetaType -> TcM [EvVar]
161 newEvVars theta = mapM newEvVar theta
162
163 --------------
164
165 newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar
166 -- Creates new *rigid* variables for predicates
167 newEvVar ty = do { name <- newSysName (predTypeOccName ty)
168 ; return (mkLocalIdOrCoVar name ty) }
169
170 newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
171 -- Deals with both equality and non-equality predicates
172 newWanted orig t_or_k pty
173 = do loc <- getCtLocM orig t_or_k
174 d <- if isEqPred pty then HoleDest <$> newCoercionHole
175 else EvVarDest <$> newEvVar pty
176 return $ CtWanted { ctev_dest = d
177 , ctev_pred = pty
178 , ctev_nosh = WDeriv
179 , ctev_loc = loc }
180
181 newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
182 newWanteds orig = mapM (newWanted orig Nothing)
183
184 cloneWanted :: Ct -> TcM CtEvidence
185 cloneWanted ct
186 = newWanted (ctEvOrigin ev) Nothing (ctEvPred ev)
187 where
188 ev = ctEvidence ct
189
190 cloneWC :: WantedConstraints -> TcM WantedConstraints
191 cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
192 = do { simples' <- mapBagM clone_one simples
193 ; implics' <- mapBagM clone_implic implics
194 ; return (wc { wc_simple = simples', wc_impl = implics' }) }
195 where
196 clone_one ct = do { ev <- cloneWanted ct; return (mkNonCanonical ev) }
197
198 clone_implic implic@(Implic { ic_wanted = inner_wanted })
199 = do { inner_wanted' <- cloneWC inner_wanted
200 ; return (implic { ic_wanted = inner_wanted' }) }
201
202 -- | Emits a new Wanted. Deals with both equalities and non-equalities.
203 emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
204 emitWanted origin pty
205 = do { ev <- newWanted origin Nothing pty
206 ; emitSimple $ mkNonCanonical ev
207 ; return $ ctEvTerm ev }
208
209 -- | Emits a new equality constraint
210 emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
211 emitWantedEq origin t_or_k role ty1 ty2
212 = do { hole <- newCoercionHole
213 ; loc <- getCtLocM origin (Just t_or_k)
214 ; emitSimple $ mkNonCanonical $
215 CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
216 , ctev_nosh = WDeriv, ctev_loc = loc }
217 ; return (mkHoleCo hole role ty1 ty2) }
218 where
219 pty = mkPrimEqPredRole role ty1 ty2
220
221 -- | Creates a new EvVar and immediately emits it as a Wanted.
222 -- No equality predicates here.
223 emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
224 emitWantedEvVar origin ty
225 = do { new_cv <- newEvVar ty
226 ; loc <- getCtLocM origin Nothing
227 ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
228 , ctev_pred = ty
229 , ctev_nosh = WDeriv
230 , ctev_loc = loc }
231 ; emitSimple $ mkNonCanonical ctev
232 ; return new_cv }
233
234 emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
235 emitWantedEvVars orig = mapM (emitWantedEvVar orig)
236
237 newDict :: Class -> [TcType] -> TcM DictId
238 newDict cls tys
239 = do { name <- newSysName (mkDictOcc (getOccName cls))
240 ; return (mkLocalId name (mkClassPred cls tys)) }
241
242 predTypeOccName :: PredType -> OccName
243 predTypeOccName ty = case classifyPredType ty of
244 ClassPred cls _ -> mkDictOcc (getOccName cls)
245 EqPred _ _ _ -> mkVarOccFS (fsLit "co")
246 IrredPred _ -> mkVarOccFS (fsLit "irred")
247
248 {-
249 ************************************************************************
250 * *
251 Coercion holes
252 * *
253 ************************************************************************
254 -}
255
256 newCoercionHole :: TcM CoercionHole
257 newCoercionHole
258 = do { u <- newUnique
259 ; traceTc "New coercion hole:" (ppr u)
260 ; ref <- newMutVar Nothing
261 ; return $ CoercionHole u ref }
262
263 -- | Put a value in a coercion hole
264 fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
265 fillCoercionHole (CoercionHole u ref) co
266 = do {
267 #if defined(DEBUG)
268 ; cts <- readTcRef ref
269 ; whenIsJust cts $ \old_co ->
270 pprPanic "Filling a filled coercion hole" (ppr u $$ ppr co $$ ppr old_co)
271 #endif
272 ; traceTc "Filling coercion hole" (ppr u <+> text ":=" <+> ppr co)
273 ; writeTcRef ref (Just co) }
274
275 -- | Is a coercion hole filled in?
276 isFilledCoercionHole :: CoercionHole -> TcM Bool
277 isFilledCoercionHole (CoercionHole _ ref) = isJust <$> readTcRef ref
278
279 -- | Retrieve the contents of a coercion hole. Panics if the hole
280 -- is unfilled
281 unpackCoercionHole :: CoercionHole -> TcM Coercion
282 unpackCoercionHole hole
283 = do { contents <- unpackCoercionHole_maybe hole
284 ; case contents of
285 Just co -> return co
286 Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) }
287
288 -- | Retrieve the contents of a coercion hole, if it is filled
289 unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
290 unpackCoercionHole_maybe (CoercionHole _ ref) = readTcRef ref
291
292 -- | Check that a coercion is appropriate for filling a hole. (The hole
293 -- itself is needed only for printing. NB: This must be /lazy/ in the coercion,
294 -- as it's used in TcHsSyn in the presence of knots.
295 -- Always returns the checked coercion, but this return value is necessary
296 -- so that the input coercion is forced only when the output is forced.
297 checkCoercionHole :: Coercion -> CoercionHole -> Role -> Type -> Type -> TcM Coercion
298 checkCoercionHole co h r t1 t2
299 -- co is already zonked, but t1 and t2 might not be
300 | debugIsOn
301 = do { t1 <- zonkTcType t1
302 ; t2 <- zonkTcType t2
303 ; let (Pair _t1 _t2, _role) = coercionKindRole co
304 ; return $
305 ASSERT2( t1 `eqType` _t1 && t2 `eqType` _t2 && r == _role
306 , (text "Bad coercion hole" <+>
307 ppr h <> colon <+> vcat [ ppr _t1, ppr _t2, ppr _role
308 , ppr co, ppr t1, ppr t2
309 , ppr r ]) )
310 co }
311 | otherwise
312 = return co
313
314 {-
315 ************************************************************************
316 *
317 Expected types
318 *
319 ************************************************************************
320
321 Note [ExpType]
322 ~~~~~~~~~~~~~~
323
324 An ExpType is used as the "expected type" when type-checking an expression.
325 An ExpType can hold a "hole" that can be filled in by the type-checker.
326 This allows us to have one tcExpr that works in both checking mode and
327 synthesis mode (that is, bidirectional type-checking). Previously, this
328 was achieved by using ordinary unification variables, but we don't need
329 or want that generality. (For example, #11397 was caused by doing the
330 wrong thing with unification variables.) Instead, we observe that these
331 holes should
332
333 1. never be nested
334 2. never appear as the type of a variable
335 3. be used linearly (never be duplicated)
336
337 By defining ExpType, separately from Type, we can achieve goals 1 and 2
338 statically.
339
340 See also [wiki:Typechecking]
341
342 Note [TcLevel of ExpType]
343 ~~~~~~~~~~~~~~~~~~~~~~~~~
344 Consider
345
346 data G a where
347 MkG :: G Bool
348
349 foo MkG = True
350
351 This is a classic untouchable-variable / ambiguous GADT return type
352 scenario. But, with ExpTypes, we'll be inferring the type of the RHS.
353 And, because there is only one branch of the case, we won't trigger
354 Note [Case branches must never infer a non-tau type] of TcMatches.
355 We thus must track a TcLevel in an Inferring ExpType. If we try to
356 fill the ExpType and find that the TcLevels don't work out, we
357 fill the ExpType with a tau-tv at the low TcLevel, hopefully to
358 be worked out later by some means. This is triggered in
359 test gadt/gadt-escape1.
360
361 -}
362
363 -- actual data definition is in TcType
364
365 -- | Make an 'ExpType' suitable for inferring a type of kind * or #.
366 newInferExpTypeNoInst :: TcM ExpSigmaType
367 newInferExpTypeNoInst = newInferExpType False
368
369 newInferExpTypeInst :: TcM ExpRhoType
370 newInferExpTypeInst = newInferExpType True
371
372 newInferExpType :: Bool -> TcM ExpType
373 newInferExpType inst
374 = do { u <- newUnique
375 ; tclvl <- getTcLevel
376 ; traceTc "newOpenInferExpType" (ppr u <+> ppr inst <+> ppr tclvl)
377 ; ref <- newMutVar Nothing
378 ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl
379 , ir_ref = ref, ir_inst = inst })) }
380
381 -- | Extract a type out of an ExpType, if one exists. But one should always
382 -- exist. Unless you're quite sure you know what you're doing.
383 readExpType_maybe :: ExpType -> TcM (Maybe TcType)
384 readExpType_maybe (Check ty) = return (Just ty)
385 readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
386
387 -- | Extract a type out of an ExpType. Otherwise, panics.
388 readExpType :: ExpType -> TcM TcType
389 readExpType exp_ty
390 = do { mb_ty <- readExpType_maybe exp_ty
391 ; case mb_ty of
392 Just ty -> return ty
393 Nothing -> pprPanic "Unknown expected type" (ppr exp_ty) }
394
395 -- | Returns the expected type when in checking mode.
396 checkingExpType_maybe :: ExpType -> Maybe TcType
397 checkingExpType_maybe (Check ty) = Just ty
398 checkingExpType_maybe _ = Nothing
399
400 -- | Returns the expected type when in checking mode. Panics if in inference
401 -- mode.
402 checkingExpType :: String -> ExpType -> TcType
403 checkingExpType _ (Check ty) = ty
404 checkingExpType err et = pprPanic "checkingExpType" (text err $$ ppr et)
405
406 tauifyExpType :: ExpType -> TcM ExpType
407 -- ^ Turn a (Infer hole) type into a (Check alpha),
408 -- where alpha is a fresh unification variable
409 tauifyExpType (Check ty) = return (Check ty) -- No-op for (Check ty)
410 tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res
411 ; return (Check ty) }
412
413 -- | Extracts the expected type if there is one, or generates a new
414 -- TauTv if there isn't.
415 expTypeToType :: ExpType -> TcM TcType
416 expTypeToType (Check ty) = return ty
417 expTypeToType (Infer inf_res) = inferResultToType inf_res
418
419 inferResultToType :: InferResult -> TcM Type
420 inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
421 , ir_ref = ref })
422 = do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
423 ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
424 -- See Note [TcLevel of ExpType]
425 ; writeMutVar ref (Just tau)
426 ; traceTc "Forcing ExpType to be monomorphic:"
427 (ppr u <+> text ":=" <+> ppr tau)
428 ; return tau }
429
430
431 {- *********************************************************************
432 * *
433 SkolemTvs (immutable)
434 * *
435 ********************************************************************* -}
436
437 tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
438 -- ^ How to instantiate the type variables
439 -> Id -- ^ Type to instantiate
440 -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result
441 -- (type vars, preds (incl equalities), rho)
442 tcInstType inst_tyvars id
443 = case tcSplitForAllTys (idType id) of
444 ([], rho) -> let -- There may be overloading despite no type variables;
445 -- (?x :: Int) => Int -> Int
446 (theta, tau) = tcSplitPhiTy rho
447 in
448 return ([], theta, tau)
449
450 (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
451 ; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho)
452 tv_prs = map tyVarName tyvars `zip` tyvars'
453 ; return (tv_prs, theta, tau) }
454
455 tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
456 -- Instantiate a type signature with skolem constants.
457 -- We could give them fresh names, but no need to do so
458 tcSkolDFunType dfun
459 = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
460 ; return (map snd tv_prs, theta, tau) }
461
462 tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
463 -- Make skolem constants, but do *not* give them new names, as above
464 -- Moreover, make them "super skolems"; see comments with superSkolemTv
465 -- see Note [Kind substitution when instantiating]
466 -- Precondition: tyvars should be ordered by scoping
467 tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
468
469 tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
470 tcSuperSkolTyVar subst tv
471 = (extendTvSubstWithClone subst tv new_tv, new_tv)
472 where
473 kind = substTyUnchecked subst (tyVarKind tv)
474 new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
475
476 -- | Given a list of @['TyVar']@, skolemize the type variables,
477 -- returning a substitution mapping the original tyvars to the
478 -- skolems, and the list of newly bound skolems. See also
479 -- tcInstSkolTyVars' for a precondition. The resulting
480 -- skolems are non-overlappable; see Note [Overlap and deriving]
481 -- for an example where this matters.
482 tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
483 tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst
484
485 tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
486 tcInstSkolTyVarsX = tcInstSkolTyVars' False
487
488 tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
489 tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
490
491 tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
492 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
493
494 tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
495 -- Precondition: tyvars should be ordered (kind vars first)
496 -- see Note [Kind substitution when instantiating]
497 -- Get the location from the monad; this is a complete freshening operation
498 tcInstSkolTyVars' overlappable subst tvs
499 = do { loc <- getSrcSpanM
500 ; lvl <- getTcLevel
501 ; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs }
502
503 mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyVarMaker
504 mkTcSkolTyVar lvl loc overlappable
505 = \ uniq old_name kind -> mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
506 kind details
507 where
508 details = SkolemTv (pushTcLevel lvl) overlappable
509 -- NB: skolems bump the level
510
511 ------------------
512 freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
513 -- ^ Give fresh uniques to a bunch of TyVars, but they stay
514 -- as TyVars, rather than becoming TcTyVars
515 -- Used in FamInst.newFamInst, and Inst.newClsInst
516 freshenTyVarBndrs = instSkolTyCoVars mk_tv
517 where
518 mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
519
520 freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcRnIf gbl lcl (TCvSubst, [CoVar])
521 -- ^ Give fresh uniques to a bunch of CoVars
522 -- Used in FamInst.newFamInst
523 freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
524 where
525 mk_cv uniq old_name kind = mkCoVar (setNameUnique old_name uniq) kind
526
527 ------------------
528 type TcTyVarMaker = Unique -> Name -> Kind -> TyCoVar
529 instSkolTyCoVars :: TcTyVarMaker -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
530 instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
531
532 instSkolTyCoVarsX :: TcTyVarMaker
533 -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
534 instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
535
536 instSkolTyCoVarX :: TcTyVarMaker
537 -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
538 instSkolTyCoVarX mk_tcv subst tycovar
539 = do { uniq <- newUnique -- using a new unique is critical. See
540 -- Note [Skolems in zonkSyntaxExpr] in TcHsSyn
541 ; let new_tcv = mk_tcv uniq old_name kind
542 subst1 | isTyVar new_tcv
543 = extendTvSubstWithClone subst tycovar new_tcv
544 | otherwise
545 = extendCvSubstWithClone subst tycovar new_tcv
546 ; return (subst1, new_tcv) }
547 where
548 old_name = tyVarName tycovar
549 kind = substTyUnchecked subst (tyVarKind tycovar)
550
551 newFskTyVar :: TcType -> TcM TcTyVar
552 newFskTyVar fam_ty
553 = do { uniq <- newUnique
554 ; ref <- newMutVar Flexi
555 ; let details = MetaTv { mtv_info = FlatSkolTv
556 , mtv_ref = ref
557 , mtv_tclvl = fmvTcLevel }
558 name = mkMetaTyVarName uniq (fsLit "fsk")
559 ; return (mkTcTyVar name (typeKind fam_ty) details) }
560
561 {-
562 Note [Kind substitution when instantiating]
563 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
564 When we instantiate a bunch of kind and type variables, first we
565 expect them to be topologically sorted.
566 Then we have to instantiate the kind variables, build a substitution
567 from old variables to the new variables, then instantiate the type
568 variables substituting the original kind.
569
570 Exemple: If we want to instantiate
571 [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
572 we want
573 [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
574 instead of the buggous
575 [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
576
577
578 ************************************************************************
579 * *
580 MetaTvs (meta type variables; mutable)
581 * *
582 ************************************************************************
583 -}
584
585 newSigTyVar :: Name -> Kind -> TcM TcTyVar
586 newSigTyVar name kind
587 = do { details <- newMetaDetails SigTv
588 ; return (mkTcTyVar name kind details) }
589
590 newFmvTyVar :: TcType -> TcM TcTyVar
591 -- Very like newMetaTyVar, except sets mtv_tclvl to one less
592 -- so that the fmv is untouchable.
593 newFmvTyVar fam_ty
594 = do { uniq <- newUnique
595 ; ref <- newMutVar Flexi
596 ; let details = MetaTv { mtv_info = FlatMetaTv
597 , mtv_ref = ref
598 , mtv_tclvl = fmvTcLevel }
599 name = mkMetaTyVarName uniq (fsLit "s")
600 ; return (mkTcTyVar name (typeKind fam_ty) details) }
601
602 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
603 newMetaDetails info
604 = do { ref <- newMutVar Flexi
605 ; tclvl <- getTcLevel
606 ; return (MetaTv { mtv_info = info
607 , mtv_ref = ref
608 , mtv_tclvl = tclvl }) }
609
610 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
611 cloneMetaTyVar tv
612 = ASSERT( isTcTyVar tv )
613 do { uniq <- newUnique
614 ; ref <- newMutVar Flexi
615 ; let name' = setNameUnique (tyVarName tv) uniq
616 details' = case tcTyVarDetails tv of
617 details@(MetaTv {}) -> details { mtv_ref = ref }
618 _ -> pprPanic "cloneMetaTyVar" (ppr tv)
619 ; return (mkTcTyVar name' (tyVarKind tv) details') }
620
621 -- Works for both type and kind variables
622 readMetaTyVar :: TyVar -> TcM MetaDetails
623 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
624 readMutVar (metaTyVarRef tyvar)
625
626 isFilledMetaTyVar :: TyVar -> TcM Bool
627 -- True of a filled-in (Indirect) meta type variable
628 isFilledMetaTyVar tv
629 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
630 = do { details <- readMutVar ref
631 ; return (isIndirect details) }
632 | otherwise = return False
633
634 isUnfilledMetaTyVar :: TyVar -> TcM Bool
635 -- True of a un-filled-in (Flexi) meta type variable
636 isUnfilledMetaTyVar tv
637 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
638 = do { details <- readMutVar ref
639 ; return (isFlexi details) }
640 | otherwise = return False
641
642 --------------------
643 -- Works with both type and kind variables
644 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
645 -- Write into a currently-empty MetaTyVar
646
647 writeMetaTyVar tyvar ty
648 | not debugIsOn
649 = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty
650
651 -- Everything from here on only happens if DEBUG is on
652 | not (isTcTyVar tyvar)
653 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
654 return ()
655
656 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
657 = writeMetaTyVarRef tyvar ref ty
658
659 | otherwise
660 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
661 return ()
662
663 --------------------
664 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
665 -- Here the tyvar is for error checking only;
666 -- the ref cell must be for the same tyvar
667 writeMetaTyVarRef tyvar ref ty
668 | not debugIsOn
669 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
670 <+> text ":=" <+> ppr ty)
671 ; writeTcRef ref (Indirect ty) }
672
673 -- Everything from here on only happens if DEBUG is on
674 | otherwise
675 = do { meta_details <- readMutVar ref;
676 -- Zonk kinds to allow the error check to work
677 ; zonked_tv_kind <- zonkTcType tv_kind
678 ; zonked_ty_kind <- zonkTcType ty_kind
679 ; let kind_check_ok = isPredTy tv_kind -- Don't check kinds for updates
680 -- to coercion variables. Why not??
681 || isConstraintKind zonked_tv_kind
682 || tcEqKind zonked_ty_kind zonked_tv_kind
683 -- Hack alert! isConstraintKind: see TcHsType
684 -- Note [Extra-constraint holes in partial type signatures]
685
686 kind_msg = hang (text "Ill-kinded update to meta tyvar")
687 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
688 <+> text ":="
689 <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) )
690
691 ; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
692
693 -- Check for double updates
694 ; MASSERT2( isFlexi meta_details, double_upd_msg meta_details )
695
696 -- Check for level OK
697 -- See Note [Level check when unifying]
698 ; MASSERT2( level_check_ok, level_check_msg )
699
700 -- Check Kinds ok
701 ; MASSERT2( kind_check_ok, kind_msg )
702
703 -- Do the write
704 ; writeMutVar ref (Indirect ty) }
705 where
706 tv_kind = tyVarKind tyvar
707 ty_kind = typeKind ty
708
709 tv_lvl = tcTyVarLevel tyvar
710 ty_lvl = tcTypeLevel ty
711
712 level_check_ok = isFlattenTyVar tyvar
713 || not (ty_lvl `strictlyDeeperThan` tv_lvl)
714 level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
715
716 double_upd_msg details = hang (text "Double update of meta tyvar")
717 2 (ppr tyvar $$ ppr details)
718
719
720 {- Note [Level check when unifying]
721 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
722 When unifying
723 alpha:lvl := ty
724 we expect that the TcLevel of 'ty' will be <= lvl.
725 However, during unflatting we do
726 fuv:l := ty:(l+1)
727 which is usually wrong; hence the check isFmmvTyVar in level_check_ok.
728 See Note [TcLevel assignment] in TcType.
729 -}
730
731 {-
732 % Generating fresh variables for pattern match check
733 -}
734
735 -- UNINSTANTIATED VERSION OF tcInstSkolTyCoVars
736 genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar]
737 -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
738 -- Precondition: tyvars should be scoping-ordered
739 -- see Note [Kind substitution when instantiating]
740 -- Get the location from the monad; this is a complete freshening operation
741 genInstSkolTyVarsX loc subst tvs
742 = instSkolTyCoVarsX (mkTcSkolTyVar topTcLevel loc False) subst tvs
743
744 {-
745 ************************************************************************
746 * *
747 MetaTvs: TauTvs
748 * *
749 ************************************************************************
750
751 Note [Never need to instantiate coercion variables]
752 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
753 With coercion variables sloshing around in types, it might seem that we
754 sometimes need to instantiate coercion variables. This would be problematic,
755 because coercion variables inhabit unboxed equality (~#), and the constraint
756 solver thinks in terms only of boxed equality (~). The solution is that
757 we never need to instantiate coercion variables in the first place.
758
759 The tyvars that we need to instantiate come from the types of functions,
760 data constructors, and patterns. These will never be quantified over
761 coercion variables, except for the special case of the promoted Eq#. But,
762 that can't ever appear in user code, so we're safe!
763 -}
764
765 mkMetaTyVarName :: Unique -> FastString -> Name
766 -- Makes a /System/ Name, which is eagerly eliminated by
767 -- the unifier; see TcUnify.nicer_to_update_tv1, and
768 -- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
769 mkMetaTyVarName uniq str = mkSystemName uniq (mkTyVarOccFS str)
770
771 newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
772 -- Make a new meta tyvar out of thin air
773 newAnonMetaTyVar meta_info kind
774 = do { uniq <- newUnique
775 ; let name = mkMetaTyVarName uniq s
776 s = case meta_info of
777 TauTv -> fsLit "t"
778 FlatMetaTv -> fsLit "fmv"
779 FlatSkolTv -> fsLit "fsk"
780 SigTv -> fsLit "a"
781 ; details <- newMetaDetails meta_info
782 ; return (mkTcTyVar name kind details) }
783
784 cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
785 -- Same as newAnonMetaTyVar, but use a supplied TyVar as the source of the print-name
786 cloneAnonMetaTyVar info tv kind
787 = do { uniq <- newUnique
788 ; details <- newMetaDetails info
789 ; let name = mkSystemName uniq (getOccName tv)
790 -- See Note [Name of an instantiated type variable]
791 ; return (mkTcTyVar name kind details) }
792
793 {- Note [Name of an instantiated type variable]
794 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
795 At the moment we give a unification variable a System Name, which
796 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
797 -}
798
799 newFlexiTyVar :: Kind -> TcM TcTyVar
800 newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
801
802 newFlexiTyVarTy :: Kind -> TcM TcType
803 newFlexiTyVarTy kind = do
804 tc_tyvar <- newFlexiTyVar kind
805 return (mkTyVarTy tc_tyvar)
806
807 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
808 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
809
810 newOpenTypeKind :: TcM TcKind
811 newOpenTypeKind
812 = do { rr <- newFlexiTyVarTy runtimeRepTy
813 ; return (tYPE rr) }
814
815 -- | Create a tyvar that can be a lifted or unlifted type.
816 -- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh
817 newOpenFlexiTyVarTy :: TcM TcType
818 newOpenFlexiTyVarTy
819 = do { kind <- newOpenTypeKind
820 ; newFlexiTyVarTy kind }
821
822 newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
823 newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
824
825 newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
826 -- Instantiate with META type variables
827 -- Note that this works for a sequence of kind, type, and coercion variables
828 -- variables. Eg [ (k:*), (a:k->k) ]
829 -- Gives [ (k7:*), (a8:k7->k7) ]
830 newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
831 -- emptyTCvSubst has an empty in-scope set, but that's fine here
832 -- Since the tyvars are freshly made, they cannot possibly be
833 -- captured by any existing for-alls.
834
835 newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
836 -- Make a new unification variable tyvar whose Name and Kind come from
837 -- an existing TyVar. We substitute kind variables in the kind.
838 newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
839
840 newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
841 -- Just like newMetaTyVars, but start with an existing substitution.
842 newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
843
844 newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
845 -- Just like newMetaTyVarX, but make a SigTv
846 newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar
847
848 newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
849 newWildCardX subst tv
850 = do { new_tv <- newAnonMetaTyVar TauTv (substTy subst (tyVarKind tv))
851 ; return (extendTvSubstWithClone subst tv new_tv, new_tv) }
852
853 new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
854 new_meta_tv_x info subst tv
855 = do { new_tv <- cloneAnonMetaTyVar info tv substd_kind
856 ; let subst1 = extendTvSubstWithClone subst tv new_tv
857 ; return (subst1, new_tv) }
858 where
859 substd_kind = substTyUnchecked subst (tyVarKind tv)
860 -- NOTE: Trac #12549 is fixed so we could use
861 -- substTy here, but the tc_infer_args problem
862 -- is not yet fixed so leaving as unchecked for now.
863 -- OLD NOTE:
864 -- Unchecked because we call newMetaTyVarX from
865 -- tcInstBinder, which is called from tc_infer_args
866 -- which does not yet take enough trouble to ensure
867 -- the in-scope set is right; e.g. Trac #12785 trips
868 -- if we use substTy here
869
870 newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
871 newMetaTyVarTyAtLevel tc_lvl kind
872 = do { uniq <- newUnique
873 ; ref <- newMutVar Flexi
874 ; let name = mkMetaTyVarName uniq (fsLit "p")
875 details = MetaTv { mtv_info = TauTv
876 , mtv_ref = ref
877 , mtv_tclvl = tc_lvl }
878 ; return (mkTyVarTy (mkTcTyVar name kind details)) }
879
880 {- *********************************************************************
881 * *
882 Quantification
883 * *
884 ************************************************************************
885
886 Note [quantifyTyVars]
887 ~~~~~~~~~~~~~~~~~~~~~
888 quantifyTyVars is given the free vars of a type that we
889 are about to wrap in a forall.
890
891 It takes these free type/kind variables (partitioned into dependent and
892 non-dependent variables) and
893 1. Zonks them and remove globals and covars
894 2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
895 3. Calls zonkQuantifiedTyVar on each
896
897 Step (2) is often unimportant, because the kind variable is often
898 also free in the type. Eg
899 Typeable k (a::k)
900 has free vars {k,a}. But the type (see Trac #7916)
901 (f::k->*) (a::k)
902 has free vars {f,a}, but we must add 'k' as well! Hence step (3).
903
904 * This function distinguishes between dependent and non-dependent
905 variables only to keep correct defaulting behavior with -XNoPolyKinds.
906 With -XPolyKinds, it treats both classes of variables identically.
907
908 * quantifyTyVars never quantifies over
909 - a coercion variable
910 - a runtime-rep variable
911
912 Note [quantifyTyVars determinism]
913 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
914 The results of quantifyTyVars are wrapped in a forall and can end up in the
915 interface file. One such example is inferred type signatures. They also affect
916 the results of optimizations, for example worker-wrapper. This means that to
917 get deterministic builds quantifyTyVars needs to be deterministic.
918
919 To achieve this CandidatesQTvs is backed by deterministic sets which allows them
920 to be later converted to a list in a deterministic order.
921
922 For more information about deterministic sets see
923 Note [Deterministic UniqFM] in UniqDFM.
924 -}
925
926 quantifyTyVars
927 :: TcTyCoVarSet -- Global tvs; already zonked
928 -> CandidatesQTvs -- See Note [Dependent type variables] in TcType
929 -- Already zonked
930 -> TcM [TcTyVar]
931 -- See Note [quantifyTyVars]
932 -- Can be given a mixture of TcTyVars and TyVars, in the case of
933 -- associated type declarations. Also accepts covars, but *never* returns any.
934
935 quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
936 = do { traceTc "quantifyTyVars" (vcat [ppr dvs, ppr gbl_tvs])
937 ; let all_cvs = filterVarSet isCoVar $ dVarSetToVarSet dep_tkvs
938 dep_kvs = dVarSetElemsWellScoped $
939 dep_tkvs `dVarSetMinusVarSet` gbl_tvs
940 `dVarSetMinusVarSet` closeOverKinds all_cvs
941 -- dVarSetElemsWellScoped: put the kind variables into
942 -- well-scoped order.
943 -- E.g. [k, (a::k)] not the other way roud
944 -- closeOverKinds all_cvs: do not quantify over coercion
945 -- variables, or any any tvs that a covar depends on
946
947 nondep_tvs = dVarSetElems $
948 (nondep_tkvs `minusDVarSet` dep_tkvs)
949 `dVarSetMinusVarSet` gbl_tvs
950 -- See Note [Dependent type variables] in TcType
951 -- The `minus` dep_tkvs removes any kind-level vars
952 -- e.g. T k (a::k) Since k appear in a kind it'll
953 -- be in dv_kvs, and is dependent. So remove it from
954 -- dv_tvs which will also contain k
955 -- No worry about dependent covars here;
956 -- they are all in dep_tkvs
957 -- No worry about scoping, because these are all
958 -- type variables
959 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
960
961 -- In the non-PolyKinds case, default the kind variables
962 -- to *, and zonk the tyvars as usual. Notice that this
963 -- may make quantifyTyVars return a shorter list
964 -- than it was passed, but that's ok
965 ; poly_kinds <- xoptM LangExt.PolyKinds
966 ; dep_kvs' <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs
967 ; nondep_tvs' <- mapMaybeM (zonk_quant False) nondep_tvs
968 -- Because of the order, any kind variables
969 -- mentioned in the kinds of the nondep_tvs'
970 -- now refer to the dep_kvs'
971
972 ; traceTc "quantifyTyVars"
973 (vcat [ text "globals:" <+> ppr gbl_tvs
974 , text "nondep:" <+> pprTyVars nondep_tvs
975 , text "dep:" <+> pprTyVars dep_kvs
976 , text "dep_kvs'" <+> pprTyVars dep_kvs'
977 , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ])
978
979 ; return (dep_kvs' ++ nondep_tvs') }
980 where
981 -- zonk_quant returns a tyvar if it should be quantified over;
982 -- otherwise, it returns Nothing. The latter case happens for
983 -- * Kind variables, with -XNoPolyKinds: don't quantify over these
984 -- * RuntimeRep variables: we never quantify over these
985 zonk_quant default_kind tkv
986 | not (isTcTyVar tkv)
987 = return (Just tkv) -- For associated types, we have the class variables
988 -- in scope, and they are TyVars not TcTyVars
989 | otherwise
990 = do { deflt_done <- defaultTyVar default_kind tkv
991 ; case deflt_done of
992 True -> return Nothing
993 False -> do { tv <- zonkQuantifiedTyVar tkv
994 ; return (Just tv) } }
995
996 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
997 -- The quantified type variables often include meta type variables
998 -- we want to freeze them into ordinary type variables
999 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
1000 -- bound occurrences of the original type variable will get zonked to
1001 -- the immutable version.
1002 --
1003 -- We leave skolem TyVars alone; they are immutable.
1004 --
1005 -- This function is called on both kind and type variables,
1006 -- but kind variables *only* if PolyKinds is on.
1007
1008 zonkQuantifiedTyVar tv
1009 = case tcTyVarDetails tv of
1010 SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
1011 ; return (setTyVarKind tv kind) }
1012 -- It might be a skolem type variable,
1013 -- for example from a user type signature
1014
1015 MetaTv {} -> skolemiseUnboundMetaTyVar tv
1016
1017 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- RuntimeUnk
1018
1019 defaultTyVar :: Bool -- True <=> please default this kind variable to *
1020 -> TcTyVar -- If it's a MetaTyVar then it is unbound
1021 -> TcM Bool -- True <=> defaulted away altogether
1022
1023 defaultTyVar default_kind tv
1024 | not (isMetaTyVar tv)
1025 = return False
1026
1027 | isRuntimeRepVar tv && not_sig_tv -- We never quantify over a RuntimeRep var
1028 = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
1029 ; writeMetaTyVar tv liftedRepTy
1030 ; return True }
1031
1032 | default_kind && not_sig_tv -- -XNoPolyKinds and this is a kind var
1033 = do { default_kind_var tv -- so default it to * if possible
1034 ; return True }
1035
1036 | otherwise
1037 = return False
1038
1039 where
1040 -- Do not default SigTvs. Doing so would violate the invariants
1041 -- on SigTvs; see Note [Signature skolems] in TcType.
1042 -- Trac #13343 is an example
1043 not_sig_tv = not (isSigTyVar tv)
1044
1045 default_kind_var :: TyVar -> TcM ()
1046 -- defaultKindVar is used exclusively with -XNoPolyKinds
1047 -- See Note [Defaulting with -XNoPolyKinds]
1048 -- It takes an (unconstrained) meta tyvar and defaults it.
1049 -- Works only on vars of type *; for other kinds, it issues an error.
1050 default_kind_var kv
1051 | isStarKind (tyVarKind kv)
1052 = do { traceTc "Defaulting a kind var to *" (ppr kv)
1053 ; writeMetaTyVar kv liftedTypeKind }
1054 | otherwise
1055 = addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
1056 , text "of kind:" <+> ppr (tyVarKind kv')
1057 , text "Perhaps enable PolyKinds or add a kind signature" ])
1058 where
1059 (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
1060
1061 skolemiseRuntimeUnk :: TcTyVar -> TcM TyVar
1062 skolemiseRuntimeUnk tv
1063 = skolemise_tv tv RuntimeUnk
1064
1065 skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar
1066 skolemiseUnboundMetaTyVar tv
1067 = skolemise_tv tv (SkolemTv (metaTyVarTcLevel tv) False)
1068
1069 skolemise_tv :: TcTyVar -> TcTyVarDetails -> TcM TyVar
1070 -- We have a Meta tyvar with a ref-cell inside it
1071 -- Skolemise it, so that
1072 -- we are totally out of Meta-tyvar-land
1073 -- We create a skolem TyVar, not a regular TyVar
1074 -- See Note [Zonking to Skolem]
1075 skolemise_tv tv details
1076 = ASSERT2( isMetaTyVar tv, ppr tv )
1077 do { when debugIsOn (check_empty tv)
1078 ; span <- getSrcSpanM -- Get the location from "here"
1079 -- ie where we are generalising
1080 ; kind <- zonkTcType (tyVarKind tv)
1081 ; let uniq = getUnique tv
1082 -- NB: Use same Unique as original tyvar. This is
1083 -- important for TcHsType.splitTelescopeTvs to work properly
1084
1085 tv_name = getOccName tv
1086 final_name = mkInternalName uniq tv_name span
1087 final_tv = mkTcTyVar final_name kind details
1088
1089 ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
1090 ; writeMetaTyVar tv (mkTyVarTy final_tv)
1091 ; return final_tv }
1092
1093 where
1094 check_empty tv -- [Sept 04] Check for non-empty.
1095 = when debugIsOn $ -- See note [Silly Type Synonym]
1096 do { cts <- readMetaTyVar tv
1097 ; case cts of
1098 Flexi -> return ()
1099 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
1100 return () }
1101
1102 {- Note [Defaulting with -XNoPolyKinds]
1103 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1104 Consider
1105
1106 data Compose f g a = Mk (f (g a))
1107
1108 We infer
1109
1110 Compose :: forall k1 k2. (k2 -> *) -> (k1 -> k2) -> k1 -> *
1111 Mk :: forall k1 k2 (f :: k2 -> *) (g :: k1 -> k2) (a :: k1).
1112 f (g a) -> Compose k1 k2 f g a
1113
1114 Now, in another module, we have -XNoPolyKinds -XDataKinds in effect.
1115 What does 'Mk mean? Pre GHC-8.0 with -XNoPolyKinds,
1116 we just defaulted all kind variables to *. But that's no good here,
1117 because the kind variables in 'Mk aren't of kind *, so defaulting to *
1118 is ill-kinded.
1119
1120 After some debate on #11334, we decided to issue an error in this case.
1121 The code is in defaultKindVar.
1122
1123 Note [What is a meta variable?]
1124 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1125 A "meta type-variable", also know as a "unification variable" is a placeholder
1126 introduced by the typechecker for an as-yet-unknown monotype.
1127
1128 For example, when we see a call `reverse (f xs)`, we know that we calling
1129 reverse :: forall a. [a] -> [a]
1130 So we know that the argument `f xs` must be a "list of something". But what is
1131 the "something"? We don't know until we explore the `f xs` a bit more. So we set
1132 out what we do know at the call of `reverse` by instantiate its type with a fresh
1133 meta tyvar, `alpha` say. So now the type of the argument `f xs`, and of the
1134 result, is `[alpha]`. The unification variable `alpha` stands for the
1135 as-yet-unknown type of the elements of the list.
1136
1137 As type inference progresses we may learn more about `alpha`. For example, suppose
1138 `f` has the type
1139 f :: forall b. b -> [Maybe b]
1140 Then we instantiate `f`'s type with another fresh unification variable, say
1141 `beta`; and equate `f`'s result type with reverse's argument type, thus
1142 `[alpha] ~ [Maybe beta]`.
1143
1144 Now we can solve this equality to learn that `alpha ~ Maybe beta`, so we've
1145 refined our knowledge about `alpha`. And so on.
1146
1147 If you found this Note useful, you may also want to have a look at
1148 Section 5 of "Practical type inference for higher rank types" (Peyton Jones,
1149 Vytiniotis, Weirich and Shields. J. Functional Programming. 2011).
1150
1151 Note [What is zonking?]
1152 ~~~~~~~~~~~~~~~~~~~~~~~
1153 GHC relies heavily on mutability in the typechecker for efficient operation.
1154 For this reason, throughout much of the type checking process meta type
1155 variables (the MetaTv constructor of TcTyVarDetails) are represented by mutable
1156 variables (known as TcRefs).
1157
1158 Zonking is the process of ripping out these mutable variables and replacing them
1159 with a real Type. This involves traversing the entire type expression, but the
1160 interesting part of replacing the mutable variables occurs in zonkTyVarOcc.
1161
1162 There are two ways to zonk a Type:
1163
1164 * zonkTcTypeToType, which is intended to be used at the end of type-checking
1165 for the final zonk. It has to deal with unfilled metavars, either by filling
1166 it with a value like Any or failing (determined by the UnboundTyVarZonker
1167 used).
1168
1169 * zonkTcType, which will happily ignore unfilled metavars. This is the
1170 appropriate function to use while in the middle of type-checking.
1171
1172 Note [Zonking to Skolem]
1173 ~~~~~~~~~~~~~~~~~~~~~~~~
1174 We used to zonk quantified type variables to regular TyVars. However, this
1175 leads to problems. Consider this program from the regression test suite:
1176
1177 eval :: Int -> String -> String -> String
1178 eval 0 root actual = evalRHS 0 root actual
1179
1180 evalRHS :: Int -> a
1181 evalRHS 0 root actual = eval 0 root actual
1182
1183 It leads to the deferral of an equality (wrapped in an implication constraint)
1184
1185 forall a. () => ((String -> String -> String) ~ a)
1186
1187 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
1188 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
1189 This has the *side effect* of also zonking the `a' in the deferred equality
1190 (which at this point is being handed around wrapped in an implication
1191 constraint).
1192
1193 Finally, the equality (with the zonked `a') will be handed back to the
1194 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
1195 If we zonk `a' with a regular type variable, we will have this regular type
1196 variable now floating around in the simplifier, which in many places assumes to
1197 only see proper TcTyVars.
1198
1199 We can avoid this problem by zonking with a skolem. The skolem is rigid
1200 (which we require for a quantified variable), but is still a TcTyVar that the
1201 simplifier knows how to deal with.
1202
1203 Note [Silly Type Synonyms]
1204 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1205 Consider this:
1206 type C u a = u -- Note 'a' unused
1207
1208 foo :: (forall a. C u a -> C u a) -> u
1209 foo x = ...
1210
1211 bar :: Num u => u
1212 bar = foo (\t -> t + t)
1213
1214 * From the (\t -> t+t) we get type {Num d} => d -> d
1215 where d is fresh.
1216
1217 * Now unify with type of foo's arg, and we get:
1218 {Num (C d a)} => C d a -> C d a
1219 where a is fresh.
1220
1221 * Now abstract over the 'a', but float out the Num (C d a) constraint
1222 because it does not 'really' mention a. (see exactTyVarsOfType)
1223 The arg to foo becomes
1224 \/\a -> \t -> t+t
1225
1226 * So we get a dict binding for Num (C d a), which is zonked to give
1227 a = ()
1228 [Note Sept 04: now that we are zonking quantified type variables
1229 on construction, the 'a' will be frozen as a regular tyvar on
1230 quantification, so the floated dict will still have type (C d a).
1231 Which renders this whole note moot; happily!]
1232
1233 * Then the \/\a abstraction has a zonked 'a' in it.
1234
1235 All very silly. I think its harmless to ignore the problem. We'll end up with
1236 a \/\a in the final result but all the occurrences of a will be zonked to ()
1237
1238 ************************************************************************
1239 * *
1240 Zonking types
1241 * *
1242 ************************************************************************
1243
1244 -}
1245
1246 -- | @tcGetGlobalTyCoVars@ returns a fully-zonked set of *scoped* tyvars free in
1247 -- the environment. To improve subsequent calls to the same function it writes
1248 -- the zonked set back into the environment. Note that this returns all
1249 -- variables free in anything (term-level or type-level) in scope. We thus
1250 -- don't have to worry about clashes with things that are not in scope, because
1251 -- if they are reachable, then they'll be returned here.
1252 tcGetGlobalTyCoVars :: TcM TcTyVarSet
1253 tcGetGlobalTyCoVars
1254 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
1255 ; gbl_tvs <- readMutVar gtv_var
1256 ; gbl_tvs' <- zonkTyCoVarsAndFV gbl_tvs
1257 ; writeMutVar gtv_var gbl_tvs'
1258 ; return gbl_tvs' }
1259
1260 -- | Zonk a type without using the smart constructors; the result type
1261 -- is available for inspection within the type-checking knot.
1262 zonkTcTypeInKnot :: TcType -> TcM TcType
1263 zonkTcTypeInKnot = mapType (zonkTcTypeMapper { tcm_smart = False }) ()
1264
1265 zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
1266 -- Zonk a type and take its free variables
1267 -- With kind polymorphism it can be essential to zonk *first*
1268 -- so that we find the right set of free variables. Eg
1269 -- forall k1. forall (a:k2). a
1270 -- where k2:=k1 is in the substitution. We don't want
1271 -- k2 to look free in this type!
1272 -- NB: This might be called from within the knot, so don't use
1273 -- smart constructors. See Note [Type-checking inside the knot] in TcHsType
1274 zonkTcTypeAndFV ty
1275 = tyCoVarsOfTypeDSet <$> zonkTcTypeInKnot ty
1276
1277 -- | Zonk a type and call 'candidateQTyVarsOfType' on it.
1278 -- Works within the knot.
1279 zonkTcTypeAndSplitDepVars :: TcType -> TcM CandidatesQTvs
1280 zonkTcTypeAndSplitDepVars ty
1281 = candidateQTyVarsOfType <$> zonkTcTypeInKnot ty
1282
1283 zonkTcTypesAndSplitDepVars :: [TcType] -> TcM CandidatesQTvs
1284 zonkTcTypesAndSplitDepVars tys
1285 = candidateQTyVarsOfTypes <$> mapM zonkTcTypeInKnot tys
1286
1287 zonkTyCoVar :: TyCoVar -> TcM TcType
1288 -- Works on TyVars and TcTyVars
1289 zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
1290 | isTyVar tv = mkTyVarTy <$> zonkTyCoVarKind tv
1291 | otherwise = ASSERT2( isCoVar tv, ppr tv )
1292 mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
1293 -- Hackily, when typechecking type and class decls
1294 -- we have TyVars in scopeadded (only) in
1295 -- TcHsType.tcTyClTyVars, but it seems
1296 -- painful to make them into TcTyVars there
1297
1298 zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
1299 zonkTyCoVarsAndFV tycovars =
1300 tyCoVarsOfTypes <$> mapM zonkTyCoVar (nonDetEltsUniqSet tycovars)
1301 -- It's OK to use nonDetEltsUniqSet here because we immediately forget about
1302 -- the ordering by turning it into a nondeterministic set and the order
1303 -- of zonking doesn't matter for determinism.
1304
1305 -- Takes a list of TyCoVars, zonks them and returns a
1306 -- deterministically ordered list of their free variables.
1307 zonkTyCoVarsAndFVList :: [TyCoVar] -> TcM [TyCoVar]
1308 zonkTyCoVarsAndFVList tycovars =
1309 tyCoVarsOfTypesList <$> mapM zonkTyCoVar tycovars
1310
1311 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
1312 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
1313
1314 ----------------- Types
1315 zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
1316 zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
1317 ; return (setTyVarKind tv kind') }
1318
1319 zonkTcTypes :: [TcType] -> TcM [TcType]
1320 zonkTcTypes tys = mapM zonkTcType tys
1321
1322 {-
1323 ************************************************************************
1324 * *
1325 Zonking constraints
1326 * *
1327 ************************************************************************
1328 -}
1329
1330 zonkImplication :: Implication -> TcM Implication
1331 zonkImplication implic@(Implic { ic_skols = skols
1332 , ic_given = given
1333 , ic_wanted = wanted
1334 , ic_info = info })
1335 = do { skols' <- mapM zonkTcTyCoVarBndr skols -- Need to zonk their kinds!
1336 -- as Trac #7230 showed
1337 ; given' <- mapM zonkEvVar given
1338 ; info' <- zonkSkolemInfo info
1339 ; wanted' <- zonkWCRec wanted
1340 ; return (implic { ic_skols = skols'
1341 , ic_given = given'
1342 , ic_wanted = wanted'
1343 , ic_info = info' }) }
1344
1345 zonkEvVar :: EvVar -> TcM EvVar
1346 zonkEvVar var = do { ty' <- zonkTcType (varType var)
1347 ; return (setVarType var ty') }
1348
1349
1350 zonkWC :: WantedConstraints -> TcM WantedConstraints
1351 zonkWC wc = zonkWCRec wc
1352
1353 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
1354 zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
1355 = do { simple' <- zonkSimples simple
1356 ; implic' <- mapBagM zonkImplication implic
1357 ; insol' <- zonkSimples insol
1358 ; return (WC { wc_simple = simple', wc_impl = implic', wc_insol = insol' }) }
1359
1360 zonkSimples :: Cts -> TcM Cts
1361 zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
1362 ; traceTc "zonkSimples done:" (ppr cts')
1363 ; return cts' }
1364
1365 zonkCt' :: Ct -> TcM Ct
1366 zonkCt' ct = zonkCt ct
1367
1368 {- Note [zonkCt behaviour]
1369 zonkCt tries to maintain the canonical form of a Ct. For example,
1370 - a CDictCan should stay a CDictCan;
1371 - a CTyEqCan should stay a CTyEqCan (if the LHS stays as a variable.).
1372 - a CHoleCan should stay a CHoleCan
1373
1374 Why?, for example:
1375 - For CDictCan, the @TcSimplify.expandSuperClasses@ step, which runs after the
1376 simple wanted and plugin loop, looks for @CDictCan@s. If a plugin is in use,
1377 constraints are zonked before being passed to the plugin. This means if we
1378 don't preserve a canonical form, @expandSuperClasses@ fails to expand
1379 superclasses. This is what happened in Trac #11525.
1380
1381 - For CHoleCan, once we forget that it's a hole, we can never recover that info.
1382
1383 NB: we do not expect to see any CFunEqCans, because zonkCt is only
1384 called on unflattened constraints.
1385 NB: Constraints are always re-flattened etc by the canonicaliser in
1386 @TcCanonical@ even if they come in as CDictCan. Only canonical constraints that
1387 are actually in the inert set carry all the guarantees. So it is okay if zonkCt
1388 creates e.g. a CDictCan where the cc_tyars are /not/ function free.
1389 -}
1390 zonkCt :: Ct -> TcM Ct
1391 zonkCt ct@(CHoleCan { cc_ev = ev })
1392 = do { ev' <- zonkCtEvidence ev
1393 ; return $ ct { cc_ev = ev' } }
1394 zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
1395 = do { ev' <- zonkCtEvidence ev
1396 ; args' <- mapM zonkTcType args
1397 ; return $ ct { cc_ev = ev', cc_tyargs = args' } }
1398 zonkCt ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs })
1399 = do { ev' <- zonkCtEvidence ev
1400 ; tv_ty' <- zonkTcTyVar tv
1401 ; case getTyVar_maybe tv_ty' of
1402 Just tv' -> do { rhs' <- zonkTcType rhs
1403 ; return ct { cc_ev = ev'
1404 , cc_tyvar = tv'
1405 , cc_rhs = rhs' } }
1406 Nothing -> return (mkNonCanonical ev') }
1407 zonkCt ct
1408 = ASSERT( not (isCFunEqCan ct) )
1409 -- We do not expect to see any CFunEqCans, because zonkCt is only called on
1410 -- unflattened constraints.
1411 do { fl' <- zonkCtEvidence (cc_ev ct)
1412 ; return (mkNonCanonical fl') }
1413
1414 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
1415 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
1416 = do { pred' <- zonkTcType pred
1417 ; return (ctev { ctev_pred = pred'}) }
1418 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest })
1419 = do { pred' <- zonkTcType pred
1420 ; let dest' = case dest of
1421 EvVarDest ev -> EvVarDest $ setVarType ev pred'
1422 -- necessary in simplifyInfer
1423 HoleDest h -> HoleDest h
1424 ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
1425 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
1426 = do { pred' <- zonkTcType pred
1427 ; return (ctev { ctev_pred = pred' }) }
1428
1429 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
1430 zonkSkolemInfo (SigSkol cx ty tv_prs) = do { ty' <- zonkTcType ty
1431 ; return (SigSkol cx ty' tv_prs) }
1432 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
1433 ; return (InferSkol ntys') }
1434 where
1435 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
1436 zonkSkolemInfo skol_info = return skol_info
1437
1438 {-
1439 %************************************************************************
1440 %* *
1441 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
1442 * *
1443 * For internal use only! *
1444 * *
1445 ************************************************************************
1446
1447 -}
1448
1449 -- zonkId is used *during* typechecking just to zonk the Id's type
1450 zonkId :: TcId -> TcM TcId
1451 zonkId id
1452 = do { ty' <- zonkTcType (idType id)
1453 ; return (Id.setIdType id ty') }
1454
1455 -- | A suitable TyCoMapper for zonking a type inside the knot, and
1456 -- before all metavars are filled in.
1457 zonkTcTypeMapper :: TyCoMapper () TcM
1458 zonkTcTypeMapper = TyCoMapper
1459 { tcm_smart = True
1460 , tcm_tyvar = const zonkTcTyVar
1461 , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
1462 , tcm_hole = hole
1463 , tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv }
1464 where
1465 hole :: () -> CoercionHole -> Role -> Type -> Type
1466 -> TcM Coercion
1467 hole _ h r t1 t2
1468 = do { contents <- unpackCoercionHole_maybe h
1469 ; case contents of
1470 Just co -> do { co <- zonkCo co
1471 ; checkCoercionHole co h r t1 t2 }
1472 Nothing -> do { t1 <- zonkTcType t1
1473 ; t2 <- zonkTcType t2
1474 ; return $ mkHoleCo h r t1 t2 } }
1475
1476
1477 -- For unbound, mutable tyvars, zonkType uses the function given to it
1478 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
1479 -- type variable and zonks the kind too
1480 zonkTcType :: TcType -> TcM TcType
1481 zonkTcType = mapType zonkTcTypeMapper ()
1482
1483 -- | "Zonk" a coercion -- really, just zonk any types in the coercion
1484 zonkCo :: Coercion -> TcM Coercion
1485 zonkCo = mapCoercion zonkTcTypeMapper ()
1486
1487 zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
1488 -- A tyvar binder is never a unification variable (MetaTv),
1489 -- rather it is always a skolems. BUT it may have a kind
1490 -- that has not yet been zonked, and may include kind
1491 -- unification variables.
1492 zonkTcTyCoVarBndr tyvar
1493 -- can't use isCoVar, because it looks at a TyCon. Argh.
1494 = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), pprTyVar tyvar )
1495 updateTyVarKindM zonkTcType tyvar
1496
1497 zonkTcTyVarBinder :: TyVarBndr TcTyVar vis -> TcM (TyVarBndr TcTyVar vis)
1498 zonkTcTyVarBinder (TvBndr tv vis)
1499 = do { tv' <- zonkTcTyCoVarBndr tv
1500 ; return (TvBndr tv' vis) }
1501
1502 zonkTcTyVar :: TcTyVar -> TcM TcType
1503 -- Simply look through all Flexis
1504 zonkTcTyVar tv
1505 | isTcTyVar tv
1506 = case tcTyVarDetails tv of
1507 SkolemTv {} -> zonk_kind_and_return
1508 RuntimeUnk {} -> zonk_kind_and_return
1509 MetaTv { mtv_ref = ref }
1510 -> do { cts <- readMutVar ref
1511 ; case cts of
1512 Flexi -> zonk_kind_and_return
1513 Indirect ty -> zonkTcType ty }
1514
1515 | otherwise -- coercion variable
1516 = zonk_kind_and_return
1517 where
1518 zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv
1519 ; return (mkTyVarTy z_tv) }
1520
1521 -- Variant that assumes that any result of zonking is still a TyVar.
1522 -- Should be used only on skolems and SigTvs
1523 zonkTcTyVarToTyVar :: TcTyVar -> TcM TcTyVar
1524 zonkTcTyVarToTyVar tv
1525 = do { ty <- zonkTcTyVar tv
1526 ; return (tcGetTyVar "zonkTcTyVarToVar" ty) }
1527
1528 {-
1529 %************************************************************************
1530 %* *
1531 Tidying
1532 * *
1533 ************************************************************************
1534 -}
1535
1536 zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
1537 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
1538 ; return (tidyOpenType env ty') }
1539
1540 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
1541 zonkTidyOrigin env (GivenOrigin skol_info)
1542 = do { skol_info1 <- zonkSkolemInfo skol_info
1543 ; let skol_info2 = tidySkolemInfo env skol_info1
1544 ; return (env, GivenOrigin skol_info2) }
1545 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act
1546 , uo_expected = exp })
1547 = do { (env1, act') <- zonkTidyTcType env act
1548 ; (env2, exp') <- zonkTidyTcType env1 exp
1549 ; return ( env2, orig { uo_actual = act'
1550 , uo_expected = exp' }) }
1551 zonkTidyOrigin env (KindEqOrigin ty1 m_ty2 orig t_or_k)
1552 = do { (env1, ty1') <- zonkTidyTcType env ty1
1553 ; (env2, m_ty2') <- case m_ty2 of
1554 Just ty2 -> second Just <$> zonkTidyTcType env1 ty2
1555 Nothing -> return (env1, Nothing)
1556 ; (env3, orig') <- zonkTidyOrigin env2 orig
1557 ; return (env3, KindEqOrigin ty1' m_ty2' orig' t_or_k) }
1558 zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
1559 = do { (env1, p1') <- zonkTidyTcType env p1
1560 ; (env2, p2') <- zonkTidyTcType env1 p2
1561 ; return (env2, FunDepOrigin1 p1' l1 p2' l2) }
1562 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
1563 = do { (env1, p1') <- zonkTidyTcType env p1
1564 ; (env2, p2') <- zonkTidyTcType env1 p2
1565 ; (env3, o1') <- zonkTidyOrigin env2 o1
1566 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
1567 zonkTidyOrigin env orig = return (env, orig)
1568
1569 ----------------
1570 tidyCt :: TidyEnv -> Ct -> Ct
1571 -- Used only in error reporting
1572 -- Also converts it to non-canonical
1573 tidyCt env ct
1574 = case ct of
1575 CHoleCan { cc_ev = ev }
1576 -> ct { cc_ev = tidy_ev env ev }
1577 _ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
1578 where
1579 tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
1580 -- NB: we do not tidy the ctev_evar field because we don't
1581 -- show it in error messages
1582 tidy_ev env ctev@(CtGiven { ctev_pred = pred })
1583 = ctev { ctev_pred = tidyType env pred }
1584 tidy_ev env ctev@(CtWanted { ctev_pred = pred })
1585 = ctev { ctev_pred = tidyType env pred }
1586 tidy_ev env ctev@(CtDerived { ctev_pred = pred })
1587 = ctev { ctev_pred = tidyType env pred }
1588
1589 ----------------
1590 tidyEvVar :: TidyEnv -> EvVar -> EvVar
1591 tidyEvVar env var = setVarType var (tidyType env (varType var))
1592
1593 ----------------
1594 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
1595 tidySkolemInfo env (DerivSkol ty) = DerivSkol (tidyType env ty)
1596 tidySkolemInfo env (SigSkol cx ty tv_prs) = tidySigSkol env cx ty tv_prs
1597 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
1598 tidySkolemInfo env (UnifyForAllSkol ty) = UnifyForAllSkol (tidyType env ty)
1599 tidySkolemInfo _ info = info
1600
1601 tidySigSkol :: TidyEnv -> UserTypeCtxt
1602 -> TcType -> [(Name,TcTyVar)] -> SkolemInfo
1603 -- We need to take special care when tidying SigSkol
1604 -- See Note [SigSkol SkolemInfo] in TcRnTypes
1605 tidySigSkol env cx ty tv_prs
1606 = SigSkol cx (tidy_ty env ty) tv_prs'
1607 where
1608 tv_prs' = mapSnd (tidyTyVarOcc env) tv_prs
1609 inst_env = mkNameEnv tv_prs'
1610
1611 tidy_ty env (ForAllTy (TvBndr tv vis) ty)
1612 = ForAllTy (TvBndr tv' vis) (tidy_ty env' ty)
1613 where
1614 (env', tv') = tidy_tv_bndr env tv
1615
1616 tidy_ty env (FunTy arg res)
1617 = FunTy (tidyType env arg) (tidy_ty env res)
1618
1619 tidy_ty env ty = tidyType env ty
1620
1621 tidy_tv_bndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
1622 tidy_tv_bndr env@(occ_env, subst) tv
1623 | Just tv' <- lookupNameEnv inst_env (tyVarName tv)
1624 = ((occ_env, extendVarEnv subst tv tv'), tv')
1625
1626 | otherwise
1627 = tidyTyCoVarBndr env tv
1628
1629 -------------------------------------------------------------------------
1630 {-
1631 %************************************************************************
1632 %* *
1633 Levity polymorphism checks
1634 * *
1635 ************************************************************************
1636
1637 See Note [Levity polymorphism checking] in DsMonad
1638
1639 -}
1640
1641 -- | According to the rules around representation polymorphism
1642 -- (see https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds), no binder
1643 -- can have a representation-polymorphic type. This check ensures
1644 -- that we respect this rule. It is a bit regrettable that this error
1645 -- occurs in zonking, after which we should have reported all errors.
1646 -- But it's hard to see where else to do it, because this can be discovered
1647 -- only after all solving is done. And, perhaps most importantly, this
1648 -- isn't really a compositional property of a type system, so it's
1649 -- not a terrible surprise that the check has to go in an awkward spot.
1650 ensureNotLevPoly :: Type -- its zonked type
1651 -> SDoc -- where this happened
1652 -> TcM ()
1653 ensureNotLevPoly ty doc
1654 = whenNoErrs $ -- sometimes we end up zonking bogus definitions of type
1655 -- forall a. a. See, for example, test ghci/scripts/T9140
1656 checkForLevPoly doc ty
1657
1658 -- See Note [Levity polymorphism checking] in DsMonad
1659 checkForLevPoly :: SDoc -> Type -> TcM ()
1660 checkForLevPoly = checkForLevPolyX addErr
1661
1662 checkForLevPolyX :: Monad m
1663 => (SDoc -> m ()) -- how to report an error
1664 -> SDoc -> Type -> m ()
1665 checkForLevPolyX add_err extra ty
1666 | isTypeLevPoly ty
1667 = add_err (formatLevPolyErr ty $$ extra)
1668 | otherwise
1669 = return ()
1670
1671 formatLevPolyErr :: Type -- levity-polymorphic type
1672 -> SDoc
1673 formatLevPolyErr ty
1674 = hang (text "A levity-polymorphic type is not allowed here:")
1675 2 (vcat [ text "Type:" <+> ppr tidy_ty
1676 , text "Kind:" <+> ppr tidy_ki ])
1677 where
1678 (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty
1679 tidy_ki = tidyType tidy_env (typeKind ty)