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