Refactor TcRnMonad.mapAndRecoverM
[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, writeMetaTyVarRef,
28 newMetaDetails, isFilledMetaTyVar_maybe, 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 new evidence variables
41 newEvVar, newEvVars, newDict,
42 newWanted, newWanteds, newHoleCt, cloneWanted, cloneWC,
43 emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
44 newTcEvBinds, newNoTcEvBinds, addTcEvBind,
45
46 newCoercionHole, fillCoercionHole, isFilledCoercionHole,
47 unpackCoercionHole, unpackCoercionHole_maybe,
48 checkCoercionHole,
49
50 --------------------------------
51 -- Instantiation
52 newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
53 newMetaTyVarTyVars, newMetaTyVarTyVarX,
54 newTyVarTyVar, newTauTyVar, newSkolemTyVar, newWildCardX,
55 tcInstType,
56 tcInstSkolTyVars,tcInstSkolTyVarsX,
57 tcInstSuperSkolTyVarsX,
58 tcSkolDFunType, tcSuperSkolTyVars,
59
60 instSkolTyCoVarsX, freshenTyVarBndrs, freshenCoVarBndrsX,
61
62 --------------------------------
63 -- Zonking and tidying
64 zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin,
65 tidyEvVar, tidyCt, tidySkolemInfo,
66 zonkTcTyVar, zonkTcTyVars,
67 zonkTcTyVarToTyVar, zonkTyVarTyVarPairs,
68 zonkTyCoVarsAndFV, zonkTcTypeAndFV,
69 zonkTyCoVarsAndFVList,
70 candidateQTyVarsOfType, candidateQTyVarsOfKind,
71 candidateQTyVarsOfTypes, CandidatesQTvs(..),
72 zonkQuantifiedTyVar, defaultTyVar,
73 quantifyTyVars,
74 zonkTcTyCoVarBndr, zonkTyConBinders,
75 zonkTcType, zonkTcTypes, zonkCo,
76 zonkTyCoVarKind,
77
78 zonkEvVar, zonkWC, zonkSimples,
79 zonkId, zonkCoVar,
80 zonkCt, zonkSkolemInfo,
81
82 tcGetGlobalTyCoVars,
83
84 ------------------------------
85 -- Levity polymorphism
86 ensureNotLevPoly, checkForLevPoly, checkForLevPolyX, formatLevPolyErr
87 ) where
88
89 #include "HsVersions.h"
90
91 -- friends:
92 import GhcPrelude
93
94 import TyCoRep
95 import TcType
96 import Type
97 import TyCon
98 import Coercion
99 import Class
100 import Var
101
102 -- others:
103 import TcRnMonad -- TcType, amongst others
104 import TcEvidence
105 import Id
106 import Name
107 import VarSet
108 import TysWiredIn
109 import TysPrim
110 import VarEnv
111 import NameEnv
112 import PrelNames
113 import Util
114 import Outputable
115 import FastString
116 import SrcLoc
117 import Bag
118 import Pair
119 import UniqSet
120 import qualified GHC.LanguageExtensions as LangExt
121
122 import Control.Monad
123 import Maybes
124 import Data.List ( mapAccumL, partition )
125 import Control.Arrow ( second )
126 import qualified Data.Semigroup as Semi
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 ; traceTc "newMetaKindVar" (ppr kv)
148 ; return (mkTyVarTy kv) }
149
150 newMetaKindVars :: Int -> TcM [TcKind]
151 newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
152
153 {-
154 ************************************************************************
155 * *
156 Evidence variables; range over constraints we can abstract over
157 * *
158 ************************************************************************
159 -}
160
161 newEvVars :: TcThetaType -> TcM [EvVar]
162 newEvVars theta = mapM newEvVar theta
163
164 --------------
165
166 newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar
167 -- Creates new *rigid* variables for predicates
168 newEvVar ty = do { name <- newSysName (predTypeOccName ty)
169 ; return (mkLocalIdOrCoVar name ty) }
170
171 newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
172 -- Deals with both equality and non-equality predicates
173 newWanted orig t_or_k pty
174 = do loc <- getCtLocM orig t_or_k
175 d <- if isEqPred pty then HoleDest <$> newCoercionHole pty
176 else EvVarDest <$> newEvVar pty
177 return $ CtWanted { ctev_dest = d
178 , ctev_pred = pty
179 , ctev_nosh = WDeriv
180 , ctev_loc = loc }
181
182 newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
183 newWanteds orig = mapM (newWanted orig Nothing)
184
185 -- | Create a new 'CHoleCan' 'Ct'.
186 newHoleCt :: Hole -> Id -> Type -> TcM Ct
187 newHoleCt hole ev ty = do
188 loc <- getCtLocM HoleOrigin Nothing
189 pure $ CHoleCan { cc_ev = CtWanted { ctev_pred = ty
190 , ctev_dest = EvVarDest ev
191 , ctev_nosh = WDeriv
192 , ctev_loc = loc }
193 , cc_hole = hole }
194
195 ----------------------------------------------
196 -- Cloning constraints
197 ----------------------------------------------
198
199 cloneWanted :: Ct -> TcM Ct
200 cloneWanted ct
201 | ev@(CtWanted { ctev_dest = HoleDest {}, ctev_pred = pty }) <- ctEvidence ct
202 = do { co_hole <- newCoercionHole pty
203 ; return (mkNonCanonical (ev { ctev_dest = HoleDest co_hole })) }
204 | otherwise
205 = return ct
206
207 cloneWC :: WantedConstraints -> TcM WantedConstraints
208 -- Clone all the evidence bindings in
209 -- a) the ic_bind field of any implications
210 -- b) the CoercionHoles of any wanted constraints
211 -- so that solving the WantedConstraints will not have any visible side
212 -- effect, /except/ from causing unifications
213 cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
214 = do { simples' <- mapBagM cloneWanted simples
215 ; implics' <- mapBagM cloneImplication implics
216 ; return (wc { wc_simple = simples', wc_impl = implics' }) }
217
218 cloneImplication :: Implication -> TcM Implication
219 cloneImplication implic@(Implic { ic_binds = binds, ic_wanted = inner_wanted })
220 = do { binds' <- cloneEvBindsVar binds
221 ; inner_wanted' <- cloneWC inner_wanted
222 ; return (implic { ic_binds = binds', ic_wanted = inner_wanted' }) }
223
224 ----------------------------------------------
225 -- Emitting constraints
226 ----------------------------------------------
227
228 -- | Emits a new Wanted. Deals with both equalities and non-equalities.
229 emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
230 emitWanted origin pty
231 = do { ev <- newWanted origin Nothing pty
232 ; emitSimple $ mkNonCanonical ev
233 ; return $ ctEvTerm ev }
234
235 -- | Emits a new equality constraint
236 emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
237 emitWantedEq origin t_or_k role ty1 ty2
238 = do { hole <- newCoercionHole pty
239 ; loc <- getCtLocM origin (Just t_or_k)
240 ; emitSimple $ mkNonCanonical $
241 CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
242 , ctev_nosh = WDeriv, ctev_loc = loc }
243 ; return (HoleCo hole) }
244 where
245 pty = mkPrimEqPredRole role ty1 ty2
246
247 -- | Creates a new EvVar and immediately emits it as a Wanted.
248 -- No equality predicates here.
249 emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
250 emitWantedEvVar origin ty
251 = do { new_cv <- newEvVar ty
252 ; loc <- getCtLocM origin Nothing
253 ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
254 , ctev_pred = ty
255 , ctev_nosh = WDeriv
256 , ctev_loc = loc }
257 ; emitSimple $ mkNonCanonical ctev
258 ; return new_cv }
259
260 emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
261 emitWantedEvVars orig = mapM (emitWantedEvVar orig)
262
263 newDict :: Class -> [TcType] -> TcM DictId
264 newDict cls tys
265 = do { name <- newSysName (mkDictOcc (getOccName cls))
266 ; return (mkLocalId name (mkClassPred cls tys)) }
267
268 predTypeOccName :: PredType -> OccName
269 predTypeOccName ty = case classifyPredType ty of
270 ClassPred cls _ -> mkDictOcc (getOccName cls)
271 EqPred {} -> mkVarOccFS (fsLit "co")
272 IrredPred {} -> mkVarOccFS (fsLit "irred")
273 ForAllPred {} -> mkVarOccFS (fsLit "df")
274
275 {-
276 ************************************************************************
277 * *
278 Coercion holes
279 * *
280 ************************************************************************
281 -}
282
283 newCoercionHole :: TcPredType -> TcM CoercionHole
284 newCoercionHole pred_ty
285 = do { co_var <- newEvVar pred_ty
286 ; traceTc "New coercion hole:" (ppr co_var)
287 ; ref <- newMutVar Nothing
288 ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } }
289
290 -- | Put a value in a coercion hole
291 fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
292 fillCoercionHole (CoercionHole { ch_ref = ref, ch_co_var = cv }) co
293 = do {
294 #if defined(DEBUG)
295 ; cts <- readTcRef ref
296 ; whenIsJust cts $ \old_co ->
297 pprPanic "Filling a filled coercion hole" (ppr cv $$ ppr co $$ ppr old_co)
298 #endif
299 ; traceTc "Filling coercion hole" (ppr cv <+> text ":=" <+> ppr co)
300 ; writeTcRef ref (Just co) }
301
302 -- | Is a coercion hole filled in?
303 isFilledCoercionHole :: CoercionHole -> TcM Bool
304 isFilledCoercionHole (CoercionHole { ch_ref = ref }) = isJust <$> readTcRef ref
305
306 -- | Retrieve the contents of a coercion hole. Panics if the hole
307 -- is unfilled
308 unpackCoercionHole :: CoercionHole -> TcM Coercion
309 unpackCoercionHole hole
310 = do { contents <- unpackCoercionHole_maybe hole
311 ; case contents of
312 Just co -> return co
313 Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) }
314
315 -- | Retrieve the contents of a coercion hole, if it is filled
316 unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
317 unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref
318
319 -- | Check that a coercion is appropriate for filling a hole. (The hole
320 -- itself is needed only for printing.
321 -- Always returns the checked coercion, but this return value is necessary
322 -- so that the input coercion is forced only when the output is forced.
323 checkCoercionHole :: CoVar -> Coercion -> TcM Coercion
324 checkCoercionHole cv co
325 | debugIsOn
326 = do { cv_ty <- zonkTcType (varType cv)
327 -- co is already zonked, but cv might not be
328 ; return $
329 ASSERT2( ok cv_ty
330 , (text "Bad coercion hole" <+>
331 ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role
332 , ppr cv_ty ]) )
333 co }
334 | otherwise
335 = return co
336
337 where
338 (Pair t1 t2, role) = coercionKindRole co
339 ok cv_ty | EqPred cv_rel cv_t1 cv_t2 <- classifyPredType cv_ty
340 = t1 `eqType` cv_t1
341 && t2 `eqType` cv_t2
342 && role == eqRelRole cv_rel
343 | otherwise
344 = False
345
346 {-
347 ************************************************************************
348 *
349 Expected types
350 *
351 ************************************************************************
352
353 Note [ExpType]
354 ~~~~~~~~~~~~~~
355
356 An ExpType is used as the "expected type" when type-checking an expression.
357 An ExpType can hold a "hole" that can be filled in by the type-checker.
358 This allows us to have one tcExpr that works in both checking mode and
359 synthesis mode (that is, bidirectional type-checking). Previously, this
360 was achieved by using ordinary unification variables, but we don't need
361 or want that generality. (For example, #11397 was caused by doing the
362 wrong thing with unification variables.) Instead, we observe that these
363 holes should
364
365 1. never be nested
366 2. never appear as the type of a variable
367 3. be used linearly (never be duplicated)
368
369 By defining ExpType, separately from Type, we can achieve goals 1 and 2
370 statically.
371
372 See also [wiki:Typechecking]
373
374 Note [TcLevel of ExpType]
375 ~~~~~~~~~~~~~~~~~~~~~~~~~
376 Consider
377
378 data G a where
379 MkG :: G Bool
380
381 foo MkG = True
382
383 This is a classic untouchable-variable / ambiguous GADT return type
384 scenario. But, with ExpTypes, we'll be inferring the type of the RHS.
385 And, because there is only one branch of the case, we won't trigger
386 Note [Case branches must never infer a non-tau type] of TcMatches.
387 We thus must track a TcLevel in an Inferring ExpType. If we try to
388 fill the ExpType and find that the TcLevels don't work out, we
389 fill the ExpType with a tau-tv at the low TcLevel, hopefully to
390 be worked out later by some means. This is triggered in
391 test gadt/gadt-escape1.
392
393 -}
394
395 -- actual data definition is in TcType
396
397 -- | Make an 'ExpType' suitable for inferring a type of kind * or #.
398 newInferExpTypeNoInst :: TcM ExpSigmaType
399 newInferExpTypeNoInst = newInferExpType False
400
401 newInferExpTypeInst :: TcM ExpRhoType
402 newInferExpTypeInst = newInferExpType True
403
404 newInferExpType :: Bool -> TcM ExpType
405 newInferExpType inst
406 = do { u <- newUnique
407 ; tclvl <- getTcLevel
408 ; traceTc "newOpenInferExpType" (ppr u <+> ppr inst <+> ppr tclvl)
409 ; ref <- newMutVar Nothing
410 ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl
411 , ir_ref = ref, ir_inst = inst })) }
412
413 -- | Extract a type out of an ExpType, if one exists. But one should always
414 -- exist. Unless you're quite sure you know what you're doing.
415 readExpType_maybe :: ExpType -> TcM (Maybe TcType)
416 readExpType_maybe (Check ty) = return (Just ty)
417 readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
418
419 -- | Extract a type out of an ExpType. Otherwise, panics.
420 readExpType :: ExpType -> TcM TcType
421 readExpType exp_ty
422 = do { mb_ty <- readExpType_maybe exp_ty
423 ; case mb_ty of
424 Just ty -> return ty
425 Nothing -> pprPanic "Unknown expected type" (ppr exp_ty) }
426
427 -- | Returns the expected type when in checking mode.
428 checkingExpType_maybe :: ExpType -> Maybe TcType
429 checkingExpType_maybe (Check ty) = Just ty
430 checkingExpType_maybe _ = Nothing
431
432 -- | Returns the expected type when in checking mode. Panics if in inference
433 -- mode.
434 checkingExpType :: String -> ExpType -> TcType
435 checkingExpType _ (Check ty) = ty
436 checkingExpType err et = pprPanic "checkingExpType" (text err $$ ppr et)
437
438 tauifyExpType :: ExpType -> TcM ExpType
439 -- ^ Turn a (Infer hole) type into a (Check alpha),
440 -- where alpha is a fresh unification variable
441 tauifyExpType (Check ty) = return (Check ty) -- No-op for (Check ty)
442 tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res
443 ; return (Check ty) }
444
445 -- | Extracts the expected type if there is one, or generates a new
446 -- TauTv if there isn't.
447 expTypeToType :: ExpType -> TcM TcType
448 expTypeToType (Check ty) = return ty
449 expTypeToType (Infer inf_res) = inferResultToType inf_res
450
451 inferResultToType :: InferResult -> TcM Type
452 inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
453 , ir_ref = ref })
454 = do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
455 ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
456 -- See Note [TcLevel of ExpType]
457 ; writeMutVar ref (Just tau)
458 ; traceTc "Forcing ExpType to be monomorphic:"
459 (ppr u <+> text ":=" <+> ppr tau)
460 ; return tau }
461
462
463 {- *********************************************************************
464 * *
465 SkolemTvs (immutable)
466 * *
467 ********************************************************************* -}
468
469 tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
470 -- ^ How to instantiate the type variables
471 -> Id -- ^ Type to instantiate
472 -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result
473 -- (type vars, preds (incl equalities), rho)
474 tcInstType inst_tyvars id
475 = case tcSplitForAllTys (idType id) of
476 ([], rho) -> let -- There may be overloading despite no type variables;
477 -- (?x :: Int) => Int -> Int
478 (theta, tau) = tcSplitPhiTy rho
479 in
480 return ([], theta, tau)
481
482 (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
483 ; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho)
484 tv_prs = map tyVarName tyvars `zip` tyvars'
485 ; return (tv_prs, theta, tau) }
486
487 tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
488 -- Instantiate a type signature with skolem constants.
489 -- We could give them fresh names, but no need to do so
490 tcSkolDFunType dfun
491 = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
492 ; return (map snd tv_prs, theta, tau) }
493
494 tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
495 -- Make skolem constants, but do *not* give them new names, as above
496 -- Moreover, make them "super skolems"; see comments with superSkolemTv
497 -- see Note [Kind substitution when instantiating]
498 -- Precondition: tyvars should be ordered by scoping
499 tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
500
501 tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
502 tcSuperSkolTyVar subst tv
503 = (extendTvSubstWithClone subst tv new_tv, new_tv)
504 where
505 kind = substTyUnchecked subst (tyVarKind tv)
506 new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
507
508 -- | Given a list of @['TyVar']@, skolemize the type variables,
509 -- returning a substitution mapping the original tyvars to the
510 -- skolems, and the list of newly bound skolems. See also
511 -- tcInstSkolTyVars' for a precondition. The resulting
512 -- skolems are non-overlappable; see Note [Overlap and deriving]
513 -- for an example where this matters.
514 tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
515 tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst
516
517 tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
518 tcInstSkolTyVarsX = tcInstSkolTyVars' False
519
520 tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
521 tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
522
523 tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
524 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
525
526 tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
527 -- Precondition: tyvars should be ordered (kind vars first)
528 -- see Note [Kind substitution when instantiating]
529 -- Get the location from the monad; this is a complete freshening operation
530 tcInstSkolTyVars' overlappable subst tvs
531 = do { loc <- getSrcSpanM
532 ; lvl <- getTcLevel
533 ; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs }
534
535 mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyCoVarMaker gbl lcl
536 -- Allocates skolems whose level is ONE GREATER THAN the passed-in tc_lvl
537 -- See Note [Skolem level allocation]
538 mkTcSkolTyVar tc_lvl loc overlappable old_name kind
539 = do { uniq <- newUnique
540 ; let name = mkInternalName uniq (getOccName old_name) loc
541 ; return (mkTcTyVar name kind details) }
542 where
543 details = SkolemTv (pushTcLevel tc_lvl) overlappable
544 -- pushTcLevel: see Note [Skolem level allocation]
545
546 {- Note [Skolem level allocation]
547 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
548 We generally allocate skolems /before/ calling pushLevelAndCaptureConstraints.
549 So we want their level to the level of the soon-to-be-created implication,
550 which has a level one higher than the current level. Hence the pushTcLevel.
551 It feels like a slight hack. Applies also to vanillaSkolemTv.
552
553 -}
554
555 ------------------
556 freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
557 -- ^ Give fresh uniques to a bunch of TyVars, but they stay
558 -- as TyVars, rather than becoming TcTyVars
559 -- Used in FamInst.newFamInst, and Inst.newClsInst
560 freshenTyVarBndrs = instSkolTyCoVars mk_tv
561 where
562 mk_tv old_name kind
563 = do { uniq <- newUnique
564 ; return (mkTyVar (setNameUnique old_name uniq) kind) }
565
566 freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcRnIf gbl lcl (TCvSubst, [CoVar])
567 -- ^ Give fresh uniques to a bunch of CoVars
568 -- Used in FamInst.newFamInst
569 freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
570 where
571 mk_cv old_name kind
572 = do { uniq <- newUnique
573 ; return (mkCoVar (setNameUnique old_name uniq) kind) }
574
575 ------------------
576 type TcTyCoVarMaker gbl lcl = Name -> Kind -> TcRnIf gbl lcl TyCoVar
577 -- The TcTyCoVarMaker should make a fresh Name, based on the old one
578 -- Freshness is critical. See Note [Skolems in zonkSyntaxExpr] in TcHsSyn
579
580 instSkolTyCoVars :: TcTyCoVarMaker gbl lcl -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
581 instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
582
583 instSkolTyCoVarsX :: TcTyCoVarMaker gbl lcl
584 -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
585 instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
586
587 instSkolTyCoVarX :: TcTyCoVarMaker gbl lcl
588 -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
589 instSkolTyCoVarX mk_tcv subst tycovar
590 = do { new_tcv <- mk_tcv old_name kind
591 ; let subst1 | isTyVar new_tcv
592 = extendTvSubstWithClone subst tycovar new_tcv
593 | otherwise
594 = extendCvSubstWithClone subst tycovar new_tcv
595 ; return (subst1, new_tcv) }
596 where
597 old_name = tyVarName tycovar
598 kind = substTyUnchecked subst (tyVarKind tycovar)
599
600 newFskTyVar :: TcType -> TcM TcTyVar
601 newFskTyVar fam_ty
602 = do { uniq <- newUnique
603 ; ref <- newMutVar Flexi
604 ; tclvl <- getTcLevel
605 ; let details = MetaTv { mtv_info = FlatSkolTv
606 , mtv_ref = ref
607 , mtv_tclvl = tclvl }
608 name = mkMetaTyVarName uniq (fsLit "fsk")
609 ; return (mkTcTyVar name (typeKind fam_ty) details) }
610
611 {-
612 Note [Kind substitution when instantiating]
613 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
614 When we instantiate a bunch of kind and type variables, first we
615 expect them to be topologically sorted.
616 Then we have to instantiate the kind variables, build a substitution
617 from old variables to the new variables, then instantiate the type
618 variables substituting the original kind.
619
620 Exemple: If we want to instantiate
621 [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
622 we want
623 [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
624 instead of the buggous
625 [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
626
627
628 ************************************************************************
629 * *
630 MetaTvs (meta type variables; mutable)
631 * *
632 ************************************************************************
633 -}
634
635 {-
636 Note [TyVarTv]
637 ~~~~~~~~~~~~
638
639 A TyVarTv can unify with type *variables* only, including other TyVarTvs and
640 skolems. Sometimes, they can unify with type variables that the user would
641 rather keep distinct; see #11203 for an example. So, any client of this
642 function needs to either allow the TyVarTvs to unify with each other or check
643 that they don't (say, with a call to findDubTyVarTvs).
644
645 Before #15050 this (under the name SigTv) was used for ScopedTypeVariables in
646 patterns, to make sure these type variables only refer to other type variables,
647 but this restriction was dropped, and ScopedTypeVariables can now refer to full
648 types (GHC Proposal 29).
649
650 The remaining uses of newTyVarTyVars are
651 * in kind signatures, see Note [Kind generalisation and TyVarTvs]
652 and Note [Use TyVarTvs in kind-checking pass]
653 * in partial type signatures, see Note [Quantified variables in partial type signatures]
654 -}
655
656 -- see Note [TyVarTv]
657 newTyVarTyVar :: Name -> Kind -> TcM TcTyVar
658 newTyVarTyVar name kind
659 = do { details <- newMetaDetails TyVarTv
660 ; let tyvar = mkTcTyVar name kind details
661 ; traceTc "newTyVarTyVar" (ppr tyvar)
662 ; return tyvar }
663
664
665 -- makes a new skolem tv
666 newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
667 newSkolemTyVar name kind = do { lvl <- getTcLevel
668 ; return (mkTcTyVar name kind (SkolemTv lvl False)) }
669
670 newFmvTyVar :: TcType -> TcM TcTyVar
671 -- Very like newMetaTyVar, except sets mtv_tclvl to one less
672 -- so that the fmv is untouchable.
673 newFmvTyVar fam_ty
674 = do { uniq <- newUnique
675 ; ref <- newMutVar Flexi
676 ; tclvl <- getTcLevel
677 ; let details = MetaTv { mtv_info = FlatMetaTv
678 , mtv_ref = ref
679 , mtv_tclvl = tclvl }
680 name = mkMetaTyVarName uniq (fsLit "s")
681 ; return (mkTcTyVar name (typeKind fam_ty) details) }
682
683 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
684 newMetaDetails info
685 = do { ref <- newMutVar Flexi
686 ; tclvl <- getTcLevel
687 ; return (MetaTv { mtv_info = info
688 , mtv_ref = ref
689 , mtv_tclvl = tclvl }) }
690
691 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
692 cloneMetaTyVar tv
693 = ASSERT( isTcTyVar tv )
694 do { uniq <- newUnique
695 ; ref <- newMutVar Flexi
696 ; let name' = setNameUnique (tyVarName tv) uniq
697 details' = case tcTyVarDetails tv of
698 details@(MetaTv {}) -> details { mtv_ref = ref }
699 _ -> pprPanic "cloneMetaTyVar" (ppr tv)
700 tyvar = mkTcTyVar name' (tyVarKind tv) details'
701 ; traceTc "cloneMetaTyVar" (ppr tyvar)
702 ; return tyvar }
703
704 -- Works for both type and kind variables
705 readMetaTyVar :: TyVar -> TcM MetaDetails
706 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
707 readMutVar (metaTyVarRef tyvar)
708
709 isFilledMetaTyVar_maybe :: TcTyVar -> TcM (Maybe Type)
710 isFilledMetaTyVar_maybe tv
711 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
712 = do { cts <- readTcRef ref
713 ; case cts of
714 Indirect ty -> return (Just ty)
715 Flexi -> return Nothing }
716 | otherwise
717 = return Nothing
718
719 isFilledMetaTyVar :: TyVar -> TcM Bool
720 -- True of a filled-in (Indirect) meta type variable
721 isFilledMetaTyVar tv = isJust <$> isFilledMetaTyVar_maybe tv
722
723 isUnfilledMetaTyVar :: TyVar -> TcM Bool
724 -- True of a un-filled-in (Flexi) meta type variable
725 -- NB: Not the opposite of isFilledMetaTyVar
726 isUnfilledMetaTyVar tv
727 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
728 = do { details <- readMutVar ref
729 ; return (isFlexi details) }
730 | otherwise = return False
731
732 --------------------
733 -- Works with both type and kind variables
734 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
735 -- Write into a currently-empty MetaTyVar
736
737 writeMetaTyVar tyvar ty
738 | not debugIsOn
739 = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty
740
741 -- Everything from here on only happens if DEBUG is on
742 | not (isTcTyVar tyvar)
743 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
744 return ()
745
746 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
747 = writeMetaTyVarRef tyvar ref ty
748
749 | otherwise
750 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
751 return ()
752
753 --------------------
754 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
755 -- Here the tyvar is for error checking only;
756 -- the ref cell must be for the same tyvar
757 writeMetaTyVarRef tyvar ref ty
758 | not debugIsOn
759 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
760 <+> text ":=" <+> ppr ty)
761 ; writeTcRef ref (Indirect ty) }
762
763 -- Everything from here on only happens if DEBUG is on
764 | otherwise
765 = do { meta_details <- readMutVar ref;
766 -- Zonk kinds to allow the error check to work
767 ; zonked_tv_kind <- zonkTcType tv_kind
768 ; zonked_ty <- zonkTcType ty
769 ; let zonked_ty_kind = typeKind zonked_ty -- need to zonk even before typeKind;
770 -- otherwise, we can panic in piResultTy
771 kind_check_ok = tcIsConstraintKind zonked_tv_kind
772 || tcEqKind zonked_ty_kind zonked_tv_kind
773 -- Hack alert! tcIsConstraintKind: see TcHsType
774 -- Note [Extra-constraint holes in partial type signatures]
775
776 kind_msg = hang (text "Ill-kinded update to meta tyvar")
777 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
778 <+> text ":="
779 <+> ppr ty <+> text "::" <+> (ppr zonked_ty_kind) )
780
781 ; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
782
783 -- Check for double updates
784 ; MASSERT2( isFlexi meta_details, double_upd_msg meta_details )
785
786 -- Check for level OK
787 -- See Note [Level check when unifying]
788 ; MASSERT2( level_check_ok, level_check_msg )
789
790 -- Check Kinds ok
791 ; MASSERT2( kind_check_ok, kind_msg )
792
793 -- Do the write
794 ; writeMutVar ref (Indirect ty) }
795 where
796 tv_kind = tyVarKind tyvar
797
798 tv_lvl = tcTyVarLevel tyvar
799 ty_lvl = tcTypeLevel ty
800
801 level_check_ok = not (ty_lvl `strictlyDeeperThan` tv_lvl)
802 level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
803
804 double_upd_msg details = hang (text "Double update of meta tyvar")
805 2 (ppr tyvar $$ ppr details)
806
807 {- Note [Level check when unifying]
808 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
809 When unifying
810 alpha:lvl := ty
811 we expect that the TcLevel of 'ty' will be <= lvl.
812 However, during unflatting we do
813 fuv:l := ty:(l+1)
814 which is usually wrong; hence the check isFmmvTyVar in level_check_ok.
815 See Note [TcLevel assignment] in TcType.
816 -}
817
818 {-
819 % Generating fresh variables for pattern match check
820 -}
821
822
823 {-
824 ************************************************************************
825 * *
826 MetaTvs: TauTvs
827 * *
828 ************************************************************************
829
830 Note [Never need to instantiate coercion variables]
831 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
832 With coercion variables sloshing around in types, it might seem that we
833 sometimes need to instantiate coercion variables. This would be problematic,
834 because coercion variables inhabit unboxed equality (~#), and the constraint
835 solver thinks in terms only of boxed equality (~). The solution is that
836 we never need to instantiate coercion variables in the first place.
837
838 The tyvars that we need to instantiate come from the types of functions,
839 data constructors, and patterns. These will never be quantified over
840 coercion variables, except for the special case of the promoted Eq#. But,
841 that can't ever appear in user code, so we're safe!
842 -}
843
844 newTauTyVar :: Name -> Kind -> TcM TcTyVar
845 newTauTyVar name kind
846 = do { details <- newMetaDetails TauTv
847 ; let tyvar = mkTcTyVar name kind details
848 ; traceTc "newTauTyVar" (ppr tyvar)
849 ; return tyvar }
850
851
852 mkMetaTyVarName :: Unique -> FastString -> Name
853 -- Makes a /System/ Name, which is eagerly eliminated by
854 -- the unifier; see TcUnify.nicer_to_update_tv1, and
855 -- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
856 mkMetaTyVarName uniq str = mkSystemName uniq (mkTyVarOccFS str)
857
858 newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
859 -- Make a new meta tyvar out of thin air
860 newAnonMetaTyVar meta_info kind
861 = do { uniq <- newUnique
862 ; let name = mkMetaTyVarName uniq s
863 s = case meta_info of
864 TauTv -> fsLit "t"
865 FlatMetaTv -> fsLit "fmv"
866 FlatSkolTv -> fsLit "fsk"
867 TyVarTv -> fsLit "a"
868 ; details <- newMetaDetails meta_info
869 ; let tyvar = mkTcTyVar name kind details
870 ; traceTc "newAnonMetaTyVar" (ppr tyvar)
871 ; return tyvar }
872
873 cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
874 -- Same as newAnonMetaTyVar, but use a supplied TyVar as the source of the print-name
875 cloneAnonMetaTyVar info tv kind
876 = do { uniq <- newUnique
877 ; details <- newMetaDetails info
878 ; let name = mkSystemName uniq (getOccName tv)
879 -- See Note [Name of an instantiated type variable]
880 tyvar = mkTcTyVar name kind details
881 ; traceTc "cloneAnonMetaTyVar" (ppr tyvar)
882 ; return tyvar }
883
884 {- Note [Name of an instantiated type variable]
885 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
886 At the moment we give a unification variable a System Name, which
887 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
888 -}
889
890 newFlexiTyVar :: Kind -> TcM TcTyVar
891 newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
892
893 newFlexiTyVarTy :: Kind -> TcM TcType
894 newFlexiTyVarTy kind = do
895 tc_tyvar <- newFlexiTyVar kind
896 return (mkTyVarTy tc_tyvar)
897
898 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
899 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
900
901 newOpenTypeKind :: TcM TcKind
902 newOpenTypeKind
903 = do { rr <- newFlexiTyVarTy runtimeRepTy
904 ; return (tYPE rr) }
905
906 -- | Create a tyvar that can be a lifted or unlifted type.
907 -- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh
908 newOpenFlexiTyVarTy :: TcM TcType
909 newOpenFlexiTyVarTy
910 = do { kind <- newOpenTypeKind
911 ; newFlexiTyVarTy kind }
912
913 newMetaTyVarTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
914 newMetaTyVarTyVars = mapAccumLM newMetaTyVarTyVarX emptyTCvSubst
915
916 newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
917 -- Instantiate with META type variables
918 -- Note that this works for a sequence of kind, type, and coercion variables
919 -- variables. Eg [ (k:*), (a:k->k) ]
920 -- Gives [ (k7:*), (a8:k7->k7) ]
921 newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
922 -- emptyTCvSubst has an empty in-scope set, but that's fine here
923 -- Since the tyvars are freshly made, they cannot possibly be
924 -- captured by any existing for-alls.
925
926 newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
927 -- Make a new unification variable tyvar whose Name and Kind come from
928 -- an existing TyVar. We substitute kind variables in the kind.
929 newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
930
931 newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
932 -- Just like newMetaTyVars, but start with an existing substitution.
933 newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
934
935 newMetaTyVarTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
936 -- Just like newMetaTyVarX, but make a TyVarTv
937 newMetaTyVarTyVarX subst tyvar = new_meta_tv_x TyVarTv subst tyvar
938
939 newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
940 newWildCardX subst tv
941 = do { new_tv <- newAnonMetaTyVar TauTv (substTy subst (tyVarKind tv))
942 ; return (extendTvSubstWithClone subst tv new_tv, new_tv) }
943
944 new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
945 new_meta_tv_x info subst tv
946 = do { new_tv <- cloneAnonMetaTyVar info tv substd_kind
947 ; let subst1 = extendTvSubstWithClone subst tv new_tv
948 ; return (subst1, new_tv) }
949 where
950 substd_kind = substTyUnchecked subst (tyVarKind tv)
951 -- NOTE: Trac #12549 is fixed so we could use
952 -- substTy here, but the tc_infer_args problem
953 -- is not yet fixed so leaving as unchecked for now.
954 -- OLD NOTE:
955 -- Unchecked because we call newMetaTyVarX from
956 -- tcInstTyBinder, which is called from tcInferApps
957 -- which does not yet take enough trouble to ensure
958 -- the in-scope set is right; e.g. Trac #12785 trips
959 -- if we use substTy here
960
961 newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
962 newMetaTyVarTyAtLevel tc_lvl kind
963 = do { uniq <- newUnique
964 ; ref <- newMutVar Flexi
965 ; let name = mkMetaTyVarName uniq (fsLit "p")
966 details = MetaTv { mtv_info = TauTv
967 , mtv_ref = ref
968 , mtv_tclvl = tc_lvl }
969 ; return (mkTyVarTy (mkTcTyVar name kind details)) }
970
971 {- *********************************************************************
972 * *
973 Finding variables to quantify over
974 * *
975 ********************************************************************* -}
976
977 data CandidatesQTvs -- See Note [Dependent type variables]
978 -- See Note [CandidatesQTvs determinism and order]
979 -- NB: All variables stored here are MetaTvs. No exceptions.
980 = DV { dv_kvs :: DTyVarSet -- "kind" metavariables (dependent)
981 , dv_tvs :: DTyVarSet -- "type" metavariables (non-dependent)
982 -- A variable may appear in both sets
983 -- E.g. T k (x::k) The first occurrence of k makes it
984 -- show up in dv_tvs, the second in dv_kvs
985 -- See Note [Dependent type variables]
986 , dv_cvs :: CoVarSet
987 -- These are covars. We will *not* quantify over these, but
988 -- we must make sure also not to quantify over any cv's kinds,
989 -- so we include them here as further direction for quantifyTyVars
990 }
991
992 instance Semi.Semigroup CandidatesQTvs where
993 (DV { dv_kvs = kv1, dv_tvs = tv1, dv_cvs = cv1 })
994 <> (DV { dv_kvs = kv2, dv_tvs = tv2, dv_cvs = cv2 })
995 = DV { dv_kvs = kv1 `unionDVarSet` kv2
996 , dv_tvs = tv1 `unionDVarSet` tv2
997 , dv_cvs = cv1 `unionVarSet` cv2 }
998
999 instance Monoid CandidatesQTvs where
1000 mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet, dv_cvs = emptyVarSet }
1001 mappend = (Semi.<>)
1002
1003 instance Outputable CandidatesQTvs where
1004 ppr (DV {dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs })
1005 = text "DV" <+> braces (pprWithCommas id [ text "dv_kvs =" <+> ppr kvs
1006 , text "dv_tvs =" <+> ppr tvs
1007 , text "dv_cvs =" <+> ppr cvs ])
1008
1009 closeOverKindsCQTvs :: TyCoVarSet -- globals
1010 -> CandidatesQTvs -> TcM CandidatesQTvs
1011 -- Don't close the covars; this is done in quantifyTyVars. Note that
1012 -- closing over the CoVars would introduce tyvars into the CoVarSet.
1013 closeOverKindsCQTvs gbl_tvs dv@(DV { dv_kvs = kvs, dv_tvs = tvs })
1014 = do { let all_kinds = map tyVarKind (dVarSetElems (kvs `unionDVarSet` tvs))
1015 ; foldlM (collect_cand_qtvs True gbl_tvs) dv all_kinds }
1016
1017 {- Note [Dependent type variables]
1018 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1019 In Haskell type inference we quantify over type variables; but we only
1020 quantify over /kind/ variables when -XPolyKinds is on. Without -XPolyKinds
1021 we default the kind variables to *.
1022
1023 So, to support this defaulting, and only for that reason, when
1024 collecting the free vars of a type, prior to quantifying, we must keep
1025 the type and kind variables separate.
1026
1027 But what does that mean in a system where kind variables /are/ type
1028 variables? It's a fairly arbitrary distinction based on how the
1029 variables appear:
1030
1031 - "Kind variables" appear in the kind of some other free variable
1032
1033 These are the ones we default to * if -XPolyKinds is off
1034
1035 - "Type variables" are all free vars that are not kind variables
1036
1037 E.g. In the type T k (a::k)
1038 'k' is a kind variable, because it occurs in the kind of 'a',
1039 even though it also appears at "top level" of the type
1040 'a' is a type variable, because it doesn't
1041
1042 We gather these variables using a CandidatesQTvs record:
1043 DV { dv_kvs: Variables free in the kind of a free type variable
1044 or of a forall-bound type variable
1045 , dv_tvs: Variables sytactically free in the type }
1046
1047 So: dv_kvs are the kind variables of the type
1048 (dv_tvs - dv_kvs) are the type variable of the type
1049
1050 Note that
1051
1052 * A variable can occur in both.
1053 T k (x::k) The first occurrence of k makes it
1054 show up in dv_tvs, the second in dv_kvs
1055
1056 * We include any coercion variables in the "dependent",
1057 "kind-variable" set because we never quantify over them.
1058
1059 * The "kind variables" might depend on each other; e.g
1060 (k1 :: k2), (k2 :: *)
1061 The "type variables" do not depend on each other; if
1062 one did, it'd be classified as a kind variable!
1063
1064 Note [CandidatesQTvs determinism and order]
1065 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1066 * Determinism: when we quantify over type variables we decide the
1067 order in which they appear in the final type. Because the order of
1068 type variables in the type can end up in the interface file and
1069 affects some optimizations like worker-wrapper, we want this order to
1070 be deterministic.
1071
1072 To achieve that we use deterministic sets of variables that can be
1073 converted to lists in a deterministic order. For more information
1074 about deterministic sets see Note [Deterministic UniqFM] in UniqDFM.
1075
1076 * Order: as well as being deterministic, we use an
1077 accumulating-parameter style for candidateQTyVarsOfType so that we
1078 add variables one at a time, left to right. That means we tend to
1079 produce the variables in left-to-right order. This is just to make
1080 it bit more predicatable for the programmer.
1081
1082 Note [Naughty quantification candidates]
1083 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1084 Consider (#14880, dependent/should_compile/T14880-2)
1085
1086 forall arg. ... (alpha[tau]:arg) ...
1087
1088 We have a metavariable alpha whose kind is a locally bound (skolem) variable.
1089 This can arise while type-checking a user-written type signature
1090 (see the test case for the full code). According to
1091 Note [Recipe for checking a signature] in TcHsType, we try to solve
1092 all constraints that arise during checking before looking to kind-generalize.
1093 However, in the case above, this solving pass does not unify alpha, because
1094 it is utterly unconstrained. The question is: what to do with alpha?
1095
1096 We can't generalize it, because it would have to be generalized *after*
1097 arg, and implicit generalization always goes before explicit generalization.
1098 We can't simply leave it be, because this type is about to go into the
1099 typing environment (as the type of some let-bound variable, say), and then
1100 chaos erupts when we try to instantiate. In any case, we'll never learn
1101 anything more about alpha anyway.
1102
1103 So, we zap it, eagerly, to Any. We don't have to do this eager zapping
1104 in terms (say, in `length []`) because terms are never re-examined before
1105 the final zonk (which zaps any lingering metavariables to Any).
1106
1107 The right time to do this eager zapping is during generalization, when
1108 every metavariable is either (A) promoted, (B) generalized, or (C) zapped
1109 (according again to Note [Recipe for checking a signature] in TcHsType).
1110
1111 Accordingly, when quantifyTyVars is skolemizing the variables to quantify,
1112 these naughty ones are zapped to Any. We identify the naughty ones by
1113 looking for out-of-scope tyvars in the candidate tyvars' kinds, where
1114 we assume that all in-scope tyvars are in the gbl_tvs passed to quantifyTyVars.
1115 In the example above, we would have `alpha` in the CandidatesQTvs, but
1116 `arg` wouldn't be in the gbl_tvs. Hence, alpha is naughty, and zapped to
1117 Any. Naughty variables are discovered by is_naughty_tv in quantifyTyVars.
1118
1119 -}
1120
1121 -- | Gathers free variables to use as quantification candidates (in
1122 -- 'quantifyTyVars'). This might output the same var
1123 -- in both sets, if it's used in both a type and a kind.
1124 -- See Note [CandidatesQTvs determinism and order]
1125 -- See Note [Dependent type variables]
1126 candidateQTyVarsOfType :: TcTyVarSet -- zonked set of global/mono tyvars
1127 -> TcType -- not necessarily zonked
1128 -> TcM CandidatesQTvs
1129 candidateQTyVarsOfType gbl_tvs ty = closeOverKindsCQTvs gbl_tvs =<<
1130 collect_cand_qtvs False gbl_tvs mempty ty
1131
1132 -- | Like 'candidateQTyVarsOfType', but consider every free variable
1133 -- to be dependent. This is appropriate when generalizing a *kind*,
1134 -- instead of a type. (That way, -XNoPolyKinds will default the variables
1135 -- to Type.)
1136 candidateQTyVarsOfKind :: TcTyVarSet -- zonked set of global/mono tyvars
1137 -> TcKind -- not necessarily zonked
1138 -> TcM CandidatesQTvs
1139 candidateQTyVarsOfKind gbl_tvs ty = closeOverKindsCQTvs gbl_tvs =<<
1140 collect_cand_qtvs True gbl_tvs mempty ty
1141
1142 collect_cand_qtvs :: Bool -- True <=> consider every fv in Type to be dependent
1143 -> VarSet -- bound variables (both locally bound and globally bound)
1144 -> CandidatesQTvs -> Type -> TcM CandidatesQTvs
1145 collect_cand_qtvs is_dep bound dvs ty
1146 = go dvs ty
1147 where
1148 go dv (AppTy t1 t2) = foldlM go dv [t1, t2]
1149 go dv (TyConApp _ tys) = foldlM go dv tys
1150 go dv (FunTy arg res) = foldlM go dv [arg, res]
1151 go dv (LitTy {}) = return dv
1152 go dv (CastTy ty co) = do dv1 <- go dv ty
1153 collect_cand_qtvs_co bound dv1 co
1154 go dv (CoercionTy co) = collect_cand_qtvs_co bound dv co
1155
1156 go dv (TyVarTy tv)
1157 | is_bound tv
1158 = return dv
1159
1160 | isImmutableTyVar tv
1161 = WARN(True, (sep [ text "Note [Naughty quantification candidates] skolem:"
1162 , ppr tv <+> dcolon <+> ppr (tyVarKind tv) ]))
1163 return dv -- This happens when processing kinds of variables affected by
1164 -- Note [Naughty quantification candidates]
1165 -- NB: CandidatesQTvs stores only MetaTvs, so don't store an
1166 -- immutable tyvar here.
1167
1168 | otherwise
1169 = ASSERT2( isMetaTyVar tv, ppr tv <+> dcolon <+> ppr (tyVarKind tv) $$ ppr ty $$ ppr bound )
1170 do { m_contents <- isFilledMetaTyVar_maybe tv
1171 ; case m_contents of
1172 Just ind_ty -> go dv ind_ty
1173
1174 Nothing -> return $ insert_tv dv tv }
1175
1176 go dv (ForAllTy (Bndr tv _) ty)
1177 = do { dv1 <- collect_cand_qtvs True bound dv (tyVarKind tv)
1178 ; collect_cand_qtvs is_dep (bound `extendVarSet` tv) dv1 ty }
1179
1180 is_bound tv = tv `elemVarSet` bound
1181
1182 insert_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv
1183 | is_dep = dv { dv_kvs = kvs `extendDVarSet` tv }
1184 | otherwise = dv { dv_tvs = tvs `extendDVarSet` tv }
1185 -- You might be tempted (like I was) to use unitDVarSet and mappend here.
1186 -- However, the union algorithm for deterministic sets depends on (roughly)
1187 -- the size of the sets. The elements from the smaller set end up to the
1188 -- right of the elements from the larger one. When sets are equal, the
1189 -- left-hand argument to `mappend` goes to the right of the right-hand
1190 -- argument. In our case, if we use unitDVarSet and mappend, we learn that
1191 -- the free variables of (a -> b -> c -> d) are [b, a, c, d], and we then
1192 -- quantify over them in that order. (The a comes after the b because we
1193 -- union the singleton sets as ({a} `mappend` {b}), producing {b, a}. Thereafter,
1194 -- the size criterion works to our advantage.) This is just annoying to
1195 -- users, so I use `extendDVarSet`, which unambiguously puts the new element
1196 -- to the right. Note that the unitDVarSet/mappend implementation would not
1197 -- be wrong against any specification -- just suboptimal and confounding to users.
1198
1199 collect_cand_qtvs_co :: VarSet -- bound variables
1200 -> CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
1201 collect_cand_qtvs_co bound = go_co
1202 where
1203 go_co dv (Refl ty) = collect_cand_qtvs True bound dv ty
1204 go_co dv (GRefl _ ty mco) = do dv1 <- collect_cand_qtvs True bound dv ty
1205 go_mco dv1 mco
1206 go_co dv (TyConAppCo _ _ cos) = foldlM go_co dv cos
1207 go_co dv (AppCo co1 co2) = foldlM go_co dv [co1, co2]
1208 go_co dv (FunCo _ co1 co2) = foldlM go_co dv [co1, co2]
1209 go_co dv (AxiomInstCo _ _ cos) = foldlM go_co dv cos
1210 go_co dv (AxiomRuleCo _ cos) = foldlM go_co dv cos
1211 go_co dv (UnivCo prov _ t1 t2) = do dv1 <- go_prov dv prov
1212 dv2 <- collect_cand_qtvs True bound dv1 t1
1213 collect_cand_qtvs True bound dv2 t2
1214 go_co dv (SymCo co) = go_co dv co
1215 go_co dv (TransCo co1 co2) = foldlM go_co dv [co1, co2]
1216 go_co dv (NthCo _ _ co) = go_co dv co
1217 go_co dv (LRCo _ co) = go_co dv co
1218 go_co dv (InstCo co1 co2) = foldlM go_co dv [co1, co2]
1219 go_co dv (KindCo co) = go_co dv co
1220 go_co dv (SubCo co) = go_co dv co
1221
1222 go_co dv (HoleCo hole) = do m_co <- unpackCoercionHole_maybe hole
1223 case m_co of
1224 Just co -> go_co dv co
1225 Nothing -> return $ insert_cv dv (coHoleCoVar hole)
1226
1227 go_co dv (CoVarCo cv)
1228 | is_bound cv
1229 = return dv
1230 | otherwise
1231 = return $ insert_cv dv cv
1232
1233 go_co dv (ForAllCo tcv kind_co co)
1234 = do { dv1 <- go_co dv kind_co
1235 ; collect_cand_qtvs_co (bound `extendVarSet` tcv) dv1 co }
1236
1237 go_mco dv MRefl = return dv
1238 go_mco dv (MCo co) = go_co dv co
1239
1240 go_prov dv UnsafeCoerceProv = return dv
1241 go_prov dv (PhantomProv co) = go_co dv co
1242 go_prov dv (ProofIrrelProv co) = go_co dv co
1243 go_prov dv (PluginProv _) = return dv
1244
1245 insert_cv dv@(DV { dv_cvs = cvs }) cv
1246 = dv { dv_cvs = cvs `extendVarSet` cv }
1247
1248 is_bound tv = tv `elemVarSet` bound
1249
1250 -- | Like 'splitDepVarsOfType', but over a list of types
1251 candidateQTyVarsOfTypes :: TyCoVarSet -- zonked global ty/covars
1252 -> [Type] -> TcM CandidatesQTvs
1253 candidateQTyVarsOfTypes gbl_tvs tys = closeOverKindsCQTvs gbl_tvs =<<
1254 foldlM (collect_cand_qtvs False gbl_tvs) mempty tys
1255
1256 {- *********************************************************************
1257 * *
1258 Quantification
1259 * *
1260 ************************************************************************
1261
1262 Note [quantifyTyVars]
1263 ~~~~~~~~~~~~~~~~~~~~~
1264 quantifyTyVars is given the free vars of a type that we
1265 are about to wrap in a forall.
1266
1267 It takes these free type/kind variables (partitioned into dependent and
1268 non-dependent variables) and
1269 1. Zonks them and remove globals and covars
1270 2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
1271 3. Calls zonkQuantifiedTyVar on each
1272
1273 Step (2) is often unimportant, because the kind variable is often
1274 also free in the type. Eg
1275 Typeable k (a::k)
1276 has free vars {k,a}. But the type (see Trac #7916)
1277 (f::k->*) (a::k)
1278 has free vars {f,a}, but we must add 'k' as well! Hence step (2).
1279
1280 * This function distinguishes between dependent and non-dependent
1281 variables only to keep correct defaulting behavior with -XNoPolyKinds.
1282 With -XPolyKinds, it treats both classes of variables identically.
1283
1284 * quantifyTyVars never quantifies over
1285 - a coercion variable (or any tv mentioned in the kind of a covar)
1286 - a runtime-rep variable
1287
1288 Note [quantifyTyVars determinism]
1289 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1290 The results of quantifyTyVars are wrapped in a forall and can end up in the
1291 interface file. One such example is inferred type signatures. They also affect
1292 the results of optimizations, for example worker-wrapper. This means that to
1293 get deterministic builds quantifyTyVars needs to be deterministic.
1294
1295 To achieve this CandidatesQTvs is backed by deterministic sets which allows them
1296 to be later converted to a list in a deterministic order.
1297
1298 For more information about deterministic sets see
1299 Note [Deterministic UniqFM] in UniqDFM.
1300 -}
1301
1302 quantifyTyVars
1303 :: TcTyCoVarSet -- Global tvs; already zonked
1304 -> CandidatesQTvs -- See Note [Dependent type variables]
1305 -- Already zonked
1306 -> TcM [TcTyVar]
1307 -- See Note [quantifyTyVars]
1308 -- Can be given a mixture of TcTyVars and TyVars, in the case of
1309 -- associated type declarations. Also accepts covars, but *never* returns any.
1310 quantifyTyVars gbl_tvs
1311 dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs, dv_cvs = covars })
1312 = do { traceTc "quantifyTyVars 1" (vcat [ppr dvs, ppr gbl_tvs])
1313 ; let mono_tvs = gbl_tvs `unionVarSet` closeOverKinds covars
1314 -- NB: All variables in the kind of a covar must not be
1315 -- quantified over, as we don't quantify over the covar.
1316
1317 dep_kvs = dVarSetElemsWellScoped $
1318 dep_tkvs `dVarSetMinusVarSet` mono_tvs
1319 -- dVarSetElemsWellScoped: put the kind variables into
1320 -- well-scoped order.
1321 -- E.g. [k, (a::k)] not the other way roud
1322
1323 nondep_tvs = dVarSetElems $
1324 (nondep_tkvs `minusDVarSet` dep_tkvs)
1325 `dVarSetMinusVarSet` mono_tvs
1326 -- See Note [Dependent type variables]
1327 -- The `minus` dep_tkvs removes any kind-level vars
1328 -- e.g. T k (a::k) Since k appear in a kind it'll
1329 -- be in dv_kvs, and is dependent. So remove it from
1330 -- dv_tvs which will also contain k
1331 -- No worry about dependent covars here;
1332 -- they are all in dep_tkvs
1333 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
1334
1335 -- See Note [Naughty quantification candidates]
1336 (naughty_deps, final_dep_kvs) = partition (is_naughty_tv mono_tvs) dep_kvs
1337 (naughty_nondeps, final_nondep_tvs) = partition (is_naughty_tv mono_tvs) nondep_tvs
1338
1339 ; mapM_ zap_naughty_tv (naughty_deps ++ naughty_nondeps)
1340
1341 -- In the non-PolyKinds case, default the kind variables
1342 -- to *, and zonk the tyvars as usual. Notice that this
1343 -- may make quantifyTyVars return a shorter list
1344 -- than it was passed, but that's ok
1345 ; poly_kinds <- xoptM LangExt.PolyKinds
1346 ; dep_kvs' <- mapMaybeM (zonk_quant (not poly_kinds)) final_dep_kvs
1347 ; nondep_tvs' <- mapMaybeM (zonk_quant False) final_nondep_tvs
1348 ; let final_qtvs = dep_kvs' ++ nondep_tvs'
1349 -- Because of the order, any kind variables
1350 -- mentioned in the kinds of the nondep_tvs'
1351 -- now refer to the dep_kvs'
1352
1353 ; traceTc "quantifyTyVars 2"
1354 (vcat [ text "globals:" <+> ppr gbl_tvs
1355 , text "mono_tvs:" <+> ppr mono_tvs
1356 , text "nondep:" <+> pprTyVars nondep_tvs
1357 , text "dep:" <+> pprTyVars dep_kvs
1358 , text "dep_kvs'" <+> pprTyVars dep_kvs'
1359 , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ])
1360
1361 -- We should never quantify over coercion variables; check this
1362 ; let co_vars = filter isCoVar final_qtvs
1363 ; MASSERT2( null co_vars, ppr co_vars )
1364
1365 ; return final_qtvs }
1366 where
1367 -- See Note [Naughty quantification candidates]
1368 is_naughty_tv mono_tvs tv
1369 = anyVarSet (isSkolemTyVar <&&> (not . (`elemVarSet` mono_tvs))) $
1370 tyCoVarsOfType (tyVarKind tv)
1371
1372 -- zonk_quant returns a tyvar if it should be quantified over;
1373 -- otherwise, it returns Nothing. The latter case happens for
1374 -- * Kind variables, with -XNoPolyKinds: don't quantify over these
1375 -- * RuntimeRep variables: we never quantify over these
1376 zonk_quant default_kind tkv
1377 | not (isTyVar tkv)
1378 = return Nothing -- this can happen for a covar that's associated with
1379 -- a coercion hole. Test case: typecheck/should_compile/T2494
1380
1381 | not (isTcTyVar tkv)
1382 = return (Just tkv) -- For associated types, we have the class variables
1383 -- in scope, and they are TyVars not TcTyVars
1384 | otherwise
1385 = do { deflt_done <- defaultTyVar default_kind tkv
1386 ; case deflt_done of
1387 True -> return Nothing
1388 False -> do { tv <- zonkQuantifiedTyVar tkv
1389 ; return (Just tv) } }
1390
1391 zap_naughty_tv tv
1392 = WARN(True, text "naughty quantification candidate: " <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv))
1393 writeMetaTyVar tv (anyTypeOfKind (tyVarKind tv))
1394
1395 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
1396 -- The quantified type variables often include meta type variables
1397 -- we want to freeze them into ordinary type variables
1398 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
1399 -- bound occurrences of the original type variable will get zonked to
1400 -- the immutable version.
1401 --
1402 -- We leave skolem TyVars alone; they are immutable.
1403 --
1404 -- This function is called on both kind and type variables,
1405 -- but kind variables *only* if PolyKinds is on.
1406
1407 zonkQuantifiedTyVar tv
1408 = case tcTyVarDetails tv of
1409 SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
1410 ; return (setTyVarKind tv kind) }
1411 -- It might be a skolem type variable,
1412 -- for example from a user type signature
1413
1414 MetaTv {} -> skolemiseUnboundMetaTyVar tv
1415
1416 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- RuntimeUnk
1417
1418 defaultTyVar :: Bool -- True <=> please default this kind variable to *
1419 -> TcTyVar -- If it's a MetaTyVar then it is unbound
1420 -> TcM Bool -- True <=> defaulted away altogether
1421
1422 defaultTyVar default_kind tv
1423 | not (isMetaTyVar tv)
1424 = return False
1425
1426 | isTyVarTyVar tv
1427 -- Do not default TyVarTvs. Doing so would violate the invariants
1428 -- on TyVarTvs; see Note [Signature skolems] in TcType.
1429 -- Trac #13343 is an example; #14555 is another
1430 -- See Note [Kind generalisation and TyVarTvs]
1431 = return False
1432
1433
1434 | isRuntimeRepVar tv -- Do not quantify over a RuntimeRep var
1435 -- unless it is a TyVarTv, handled earlier
1436 = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
1437 ; writeMetaTyVar tv liftedRepTy
1438 ; return True }
1439
1440 | default_kind -- -XNoPolyKinds and this is a kind var
1441 = do { default_kind_var tv -- so default it to * if possible
1442 ; return True }
1443
1444 | otherwise
1445 = return False
1446
1447 where
1448 default_kind_var :: TyVar -> TcM ()
1449 -- defaultKindVar is used exclusively with -XNoPolyKinds
1450 -- See Note [Defaulting with -XNoPolyKinds]
1451 -- It takes an (unconstrained) meta tyvar and defaults it.
1452 -- Works only on vars of type *; for other kinds, it issues an error.
1453 default_kind_var kv
1454 | isLiftedTypeKind (tyVarKind kv)
1455 = do { traceTc "Defaulting a kind var to *" (ppr kv)
1456 ; writeMetaTyVar kv liftedTypeKind }
1457 | otherwise
1458 = addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
1459 , text "of kind:" <+> ppr (tyVarKind kv')
1460 , text "Perhaps enable PolyKinds or add a kind signature" ])
1461 where
1462 (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
1463
1464 skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar
1465 -- We have a Meta tyvar with a ref-cell inside it
1466 -- Skolemise it, so that we are totally out of Meta-tyvar-land
1467 -- We create a skolem TcTyVar, not a regular TyVar
1468 -- See Note [Zonking to Skolem]
1469 skolemiseUnboundMetaTyVar tv
1470 = ASSERT2( isMetaTyVar tv, ppr tv )
1471 do { when debugIsOn (check_empty tv)
1472 ; span <- getSrcSpanM -- Get the location from "here"
1473 -- ie where we are generalising
1474 ; kind <- zonkTcType (tyVarKind tv)
1475 ; let uniq = getUnique tv
1476 -- NB: Use same Unique as original tyvar. This is
1477 -- convenient in reading dumps, but is otherwise inessential.
1478
1479 tv_name = getOccName tv
1480 final_name = mkInternalName uniq tv_name span
1481 final_tv = mkTcTyVar final_name kind details
1482
1483 ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
1484 ; writeMetaTyVar tv (mkTyVarTy final_tv)
1485 ; return final_tv }
1486
1487 where
1488 details = SkolemTv (metaTyVarTcLevel tv) False
1489 check_empty tv -- [Sept 04] Check for non-empty.
1490 = when debugIsOn $ -- See note [Silly Type Synonym]
1491 do { cts <- readMetaTyVar tv
1492 ; case cts of
1493 Flexi -> return ()
1494 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
1495 return () }
1496
1497 {- Note [Defaulting with -XNoPolyKinds]
1498 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1499 Consider
1500
1501 data Compose f g a = Mk (f (g a))
1502
1503 We infer
1504
1505 Compose :: forall k1 k2. (k2 -> *) -> (k1 -> k2) -> k1 -> *
1506 Mk :: forall k1 k2 (f :: k2 -> *) (g :: k1 -> k2) (a :: k1).
1507 f (g a) -> Compose k1 k2 f g a
1508
1509 Now, in another module, we have -XNoPolyKinds -XDataKinds in effect.
1510 What does 'Mk mean? Pre GHC-8.0 with -XNoPolyKinds,
1511 we just defaulted all kind variables to *. But that's no good here,
1512 because the kind variables in 'Mk aren't of kind *, so defaulting to *
1513 is ill-kinded.
1514
1515 After some debate on #11334, we decided to issue an error in this case.
1516 The code is in defaultKindVar.
1517
1518 Note [What is a meta variable?]
1519 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1520 A "meta type-variable", also know as a "unification variable" is a placeholder
1521 introduced by the typechecker for an as-yet-unknown monotype.
1522
1523 For example, when we see a call `reverse (f xs)`, we know that we calling
1524 reverse :: forall a. [a] -> [a]
1525 So we know that the argument `f xs` must be a "list of something". But what is
1526 the "something"? We don't know until we explore the `f xs` a bit more. So we set
1527 out what we do know at the call of `reverse` by instantiate its type with a fresh
1528 meta tyvar, `alpha` say. So now the type of the argument `f xs`, and of the
1529 result, is `[alpha]`. The unification variable `alpha` stands for the
1530 as-yet-unknown type of the elements of the list.
1531
1532 As type inference progresses we may learn more about `alpha`. For example, suppose
1533 `f` has the type
1534 f :: forall b. b -> [Maybe b]
1535 Then we instantiate `f`'s type with another fresh unification variable, say
1536 `beta`; and equate `f`'s result type with reverse's argument type, thus
1537 `[alpha] ~ [Maybe beta]`.
1538
1539 Now we can solve this equality to learn that `alpha ~ Maybe beta`, so we've
1540 refined our knowledge about `alpha`. And so on.
1541
1542 If you found this Note useful, you may also want to have a look at
1543 Section 5 of "Practical type inference for higher rank types" (Peyton Jones,
1544 Vytiniotis, Weirich and Shields. J. Functional Programming. 2011).
1545
1546 Note [What is zonking?]
1547 ~~~~~~~~~~~~~~~~~~~~~~~
1548 GHC relies heavily on mutability in the typechecker for efficient operation.
1549 For this reason, throughout much of the type checking process meta type
1550 variables (the MetaTv constructor of TcTyVarDetails) are represented by mutable
1551 variables (known as TcRefs).
1552
1553 Zonking is the process of ripping out these mutable variables and replacing them
1554 with a real Type. This involves traversing the entire type expression, but the
1555 interesting part of replacing the mutable variables occurs in zonkTyVarOcc.
1556
1557 There are two ways to zonk a Type:
1558
1559 * zonkTcTypeToType, which is intended to be used at the end of type-checking
1560 for the final zonk. It has to deal with unfilled metavars, either by filling
1561 it with a value like Any or failing (determined by the UnboundTyVarZonker
1562 used).
1563
1564 * zonkTcType, which will happily ignore unfilled metavars. This is the
1565 appropriate function to use while in the middle of type-checking.
1566
1567 Note [Zonking to Skolem]
1568 ~~~~~~~~~~~~~~~~~~~~~~~~
1569 We used to zonk quantified type variables to regular TyVars. However, this
1570 leads to problems. Consider this program from the regression test suite:
1571
1572 eval :: Int -> String -> String -> String
1573 eval 0 root actual = evalRHS 0 root actual
1574
1575 evalRHS :: Int -> a
1576 evalRHS 0 root actual = eval 0 root actual
1577
1578 It leads to the deferral of an equality (wrapped in an implication constraint)
1579
1580 forall a. () => ((String -> String -> String) ~ a)
1581
1582 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
1583 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
1584 This has the *side effect* of also zonking the `a' in the deferred equality
1585 (which at this point is being handed around wrapped in an implication
1586 constraint).
1587
1588 Finally, the equality (with the zonked `a') will be handed back to the
1589 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
1590 If we zonk `a' with a regular type variable, we will have this regular type
1591 variable now floating around in the simplifier, which in many places assumes to
1592 only see proper TcTyVars.
1593
1594 We can avoid this problem by zonking with a skolem. The skolem is rigid
1595 (which we require for a quantified variable), but is still a TcTyVar that the
1596 simplifier knows how to deal with.
1597
1598 Note [Silly Type Synonyms]
1599 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1600 Consider this:
1601 type C u a = u -- Note 'a' unused
1602
1603 foo :: (forall a. C u a -> C u a) -> u
1604 foo x = ...
1605
1606 bar :: Num u => u
1607 bar = foo (\t -> t + t)
1608
1609 * From the (\t -> t+t) we get type {Num d} => d -> d
1610 where d is fresh.
1611
1612 * Now unify with type of foo's arg, and we get:
1613 {Num (C d a)} => C d a -> C d a
1614 where a is fresh.
1615
1616 * Now abstract over the 'a', but float out the Num (C d a) constraint
1617 because it does not 'really' mention a. (see exactTyVarsOfType)
1618 The arg to foo becomes
1619 \/\a -> \t -> t+t
1620
1621 * So we get a dict binding for Num (C d a), which is zonked to give
1622 a = ()
1623 [Note Sept 04: now that we are zonking quantified type variables
1624 on construction, the 'a' will be frozen as a regular tyvar on
1625 quantification, so the floated dict will still have type (C d a).
1626 Which renders this whole note moot; happily!]
1627
1628 * Then the \/\a abstraction has a zonked 'a' in it.
1629
1630 All very silly. I think its harmless to ignore the problem. We'll end up with
1631 a \/\a in the final result but all the occurrences of a will be zonked to ()
1632
1633 ************************************************************************
1634 * *
1635 Zonking types
1636 * *
1637 ************************************************************************
1638
1639 -}
1640
1641 -- | @tcGetGlobalTyCoVars@ returns a fully-zonked set of *scoped* tyvars free in
1642 -- the environment. To improve subsequent calls to the same function it writes
1643 -- the zonked set back into the environment. Note that this returns all
1644 -- variables free in anything (term-level or type-level) in scope. We thus
1645 -- don't have to worry about clashes with things that are not in scope, because
1646 -- if they are reachable, then they'll be returned here.
1647 -- NB: This is closed over kinds, so it can return unification variables mentioned
1648 -- in the kinds of in-scope tyvars.
1649 tcGetGlobalTyCoVars :: TcM TcTyVarSet
1650 tcGetGlobalTyCoVars
1651 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
1652 ; gbl_tvs <- readMutVar gtv_var
1653 ; gbl_tvs' <- zonkTyCoVarsAndFV gbl_tvs
1654 ; writeMutVar gtv_var gbl_tvs'
1655 ; return gbl_tvs' }
1656
1657 zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
1658 -- Zonk a type and take its free variables
1659 -- With kind polymorphism it can be essential to zonk *first*
1660 -- so that we find the right set of free variables. Eg
1661 -- forall k1. forall (a:k2). a
1662 -- where k2:=k1 is in the substitution. We don't want
1663 -- k2 to look free in this type!
1664 zonkTcTypeAndFV ty
1665 = tyCoVarsOfTypeDSet <$> zonkTcType ty
1666
1667 zonkTyCoVar :: TyCoVar -> TcM TcType
1668 -- Works on TyVars and TcTyVars
1669 zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
1670 | isTyVar tv = mkTyVarTy <$> zonkTyCoVarKind tv
1671 | otherwise = ASSERT2( isCoVar tv, ppr tv )
1672 mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
1673 -- Hackily, when typechecking type and class decls
1674 -- we have TyVars in scopeadded (only) in
1675 -- TcHsType.tcTyClTyVars, but it seems
1676 -- painful to make them into TcTyVars there
1677
1678 zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
1679 zonkTyCoVarsAndFV tycovars =
1680 tyCoVarsOfTypes <$> mapM zonkTyCoVar (nonDetEltsUniqSet tycovars)
1681 -- It's OK to use nonDetEltsUniqSet here because we immediately forget about
1682 -- the ordering by turning it into a nondeterministic set and the order
1683 -- of zonking doesn't matter for determinism.
1684
1685 -- Takes a list of TyCoVars, zonks them and returns a
1686 -- deterministically ordered list of their free variables.
1687 zonkTyCoVarsAndFVList :: [TyCoVar] -> TcM [TyCoVar]
1688 zonkTyCoVarsAndFVList tycovars =
1689 tyCoVarsOfTypesList <$> mapM zonkTyCoVar tycovars
1690
1691 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
1692 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
1693
1694 ----------------- Types
1695 zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
1696 zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
1697 ; return (setTyVarKind tv kind') }
1698
1699 zonkTcTypes :: [TcType] -> TcM [TcType]
1700 zonkTcTypes tys = mapM zonkTcType tys
1701
1702 {-
1703 ************************************************************************
1704 * *
1705 Zonking constraints
1706 * *
1707 ************************************************************************
1708 -}
1709
1710 zonkImplication :: Implication -> TcM Implication
1711 zonkImplication implic@(Implic { ic_skols = skols
1712 , ic_given = given
1713 , ic_wanted = wanted
1714 , ic_info = info })
1715 = do { skols' <- mapM zonkTyCoVarKind skols -- Need to zonk their kinds!
1716 -- as Trac #7230 showed
1717 ; given' <- mapM zonkEvVar given
1718 ; info' <- zonkSkolemInfo info
1719 ; wanted' <- zonkWCRec wanted
1720 ; return (implic { ic_skols = skols'
1721 , ic_given = given'
1722 , ic_wanted = wanted'
1723 , ic_info = info' }) }
1724
1725 zonkEvVar :: EvVar -> TcM EvVar
1726 zonkEvVar var = do { ty' <- zonkTcType (varType var)
1727 ; return (setVarType var ty') }
1728
1729
1730 zonkWC :: WantedConstraints -> TcM WantedConstraints
1731 zonkWC wc = zonkWCRec wc
1732
1733 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
1734 zonkWCRec (WC { wc_simple = simple, wc_impl = implic })
1735 = do { simple' <- zonkSimples simple
1736 ; implic' <- mapBagM zonkImplication implic
1737 ; return (WC { wc_simple = simple', wc_impl = implic' }) }
1738
1739 zonkSimples :: Cts -> TcM Cts
1740 zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
1741 ; traceTc "zonkSimples done:" (ppr cts')
1742 ; return cts' }
1743
1744 zonkCt' :: Ct -> TcM Ct
1745 zonkCt' ct = zonkCt ct
1746
1747 {- Note [zonkCt behaviour]
1748 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1749 zonkCt tries to maintain the canonical form of a Ct. For example,
1750 - a CDictCan should stay a CDictCan;
1751 - a CTyEqCan should stay a CTyEqCan (if the LHS stays as a variable.).
1752 - a CHoleCan should stay a CHoleCan
1753 - a CIrredCan should stay a CIrredCan with its cc_insol flag intact
1754
1755 Why?, for example:
1756 - For CDictCan, the @TcSimplify.expandSuperClasses@ step, which runs after the
1757 simple wanted and plugin loop, looks for @CDictCan@s. If a plugin is in use,
1758 constraints are zonked before being passed to the plugin. This means if we
1759 don't preserve a canonical form, @expandSuperClasses@ fails to expand
1760 superclasses. This is what happened in Trac #11525.
1761
1762 - For CHoleCan, once we forget that it's a hole, we can never recover that info.
1763
1764 - For CIrredCan we want to see if a constraint is insoluble with insolubleWC
1765
1766 NB: we do not expect to see any CFunEqCans, because zonkCt is only
1767 called on unflattened constraints.
1768
1769 NB: Constraints are always re-flattened etc by the canonicaliser in
1770 @TcCanonical@ even if they come in as CDictCan. Only canonical constraints that
1771 are actually in the inert set carry all the guarantees. So it is okay if zonkCt
1772 creates e.g. a CDictCan where the cc_tyars are /not/ function free.
1773 -}
1774
1775 zonkCt :: Ct -> TcM Ct
1776 zonkCt ct@(CHoleCan { cc_ev = ev })
1777 = do { ev' <- zonkCtEvidence ev
1778 ; return $ ct { cc_ev = ev' } }
1779
1780 zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
1781 = do { ev' <- zonkCtEvidence ev
1782 ; args' <- mapM zonkTcType args
1783 ; return $ ct { cc_ev = ev', cc_tyargs = args' } }
1784
1785 zonkCt ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs })
1786 = do { ev' <- zonkCtEvidence ev
1787 ; tv_ty' <- zonkTcTyVar tv
1788 ; case getTyVar_maybe tv_ty' of
1789 Just tv' -> do { rhs' <- zonkTcType rhs
1790 ; return ct { cc_ev = ev'
1791 , cc_tyvar = tv'
1792 , cc_rhs = rhs' } }
1793 Nothing -> return (mkNonCanonical ev') }
1794
1795 zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_insol flag
1796 = do { ev' <- zonkCtEvidence ev
1797 ; return (ct { cc_ev = ev' }) }
1798
1799 zonkCt ct
1800 = ASSERT( not (isCFunEqCan ct) )
1801 -- We do not expect to see any CFunEqCans, because zonkCt is only called on
1802 -- unflattened constraints.
1803 do { fl' <- zonkCtEvidence (ctEvidence ct)
1804 ; return (mkNonCanonical fl') }
1805
1806 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
1807 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
1808 = do { pred' <- zonkTcType pred
1809 ; return (ctev { ctev_pred = pred'}) }
1810 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest })
1811 = do { pred' <- zonkTcType pred
1812 ; let dest' = case dest of
1813 EvVarDest ev -> EvVarDest $ setVarType ev pred'
1814 -- necessary in simplifyInfer
1815 HoleDest h -> HoleDest h
1816 ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
1817 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
1818 = do { pred' <- zonkTcType pred
1819 ; return (ctev { ctev_pred = pred' }) }
1820
1821 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
1822 zonkSkolemInfo (SigSkol cx ty tv_prs) = do { ty' <- zonkTcType ty
1823 ; return (SigSkol cx ty' tv_prs) }
1824 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
1825 ; return (InferSkol ntys') }
1826 where
1827 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
1828 zonkSkolemInfo skol_info = return skol_info
1829
1830 {-
1831 %************************************************************************
1832 %* *
1833 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
1834 * *
1835 * For internal use only! *
1836 * *
1837 ************************************************************************
1838
1839 -}
1840
1841 -- zonkId is used *during* typechecking just to zonk the Id's type
1842 zonkId :: TcId -> TcM TcId
1843 zonkId id
1844 = do { ty' <- zonkTcType (idType id)
1845 ; return (Id.setIdType id ty') }
1846
1847 zonkCoVar :: CoVar -> TcM CoVar
1848 zonkCoVar = zonkId
1849
1850 -- | A suitable TyCoMapper for zonking a type during type-checking,
1851 -- before all metavars are filled in.
1852 zonkTcTypeMapper :: TyCoMapper () TcM
1853 zonkTcTypeMapper = TyCoMapper
1854 { tcm_smart = True
1855 , tcm_tyvar = const zonkTcTyVar
1856 , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
1857 , tcm_hole = hole
1858 , tcm_tycobinder = \_env tv _vis -> ((), ) <$> zonkTyCoVarKind tv
1859 , tcm_tycon = return }
1860 where
1861 hole :: () -> CoercionHole -> TcM Coercion
1862 hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
1863 = do { contents <- readTcRef ref
1864 ; case contents of
1865 Just co -> do { co' <- zonkCo co
1866 ; checkCoercionHole cv co' }
1867 Nothing -> do { cv' <- zonkCoVar cv
1868 ; return $ HoleCo (hole { ch_co_var = cv' }) } }
1869
1870 -- For unbound, mutable tyvars, zonkType uses the function given to it
1871 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
1872 -- type variable and zonks the kind too
1873 zonkTcType :: TcType -> TcM TcType
1874 zonkTcType = mapType zonkTcTypeMapper ()
1875
1876 -- | "Zonk" a coercion -- really, just zonk any types in the coercion
1877 zonkCo :: Coercion -> TcM Coercion
1878 zonkCo = mapCoercion zonkTcTypeMapper ()
1879
1880 zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
1881 -- A tyvar binder is never a unification variable (TauTv),
1882 -- rather it is always a skolem. It *might* be a TyVarTv.
1883 -- (Because non-CUSK type declarations use TyVarTvs.)
1884 -- Regardless, it may have a kind
1885 -- that has not yet been zonked, and may include kind
1886 -- unification variables.
1887 zonkTcTyCoVarBndr tyvar
1888 | isTyVarTyVar tyvar
1889 -- We want to preserve the binding location of the original TyVarTv.
1890 -- This is important for error messages. If we don't do this, then
1891 -- we get bad locations in, e.g., typecheck/should_fail/T2688
1892 = do { zonked_ty <- zonkTcTyVar tyvar
1893 ; let zonked_tyvar = tcGetTyVar "zonkTcTyCoVarBndr TyVarTv" zonked_ty
1894 zonked_name = getName zonked_tyvar
1895 reloc'd_name = setNameLoc zonked_name (getSrcSpan tyvar)
1896 ; return (setTyVarName zonked_tyvar reloc'd_name) }
1897
1898 | otherwise
1899 = ASSERT2( isImmutableTyVar tyvar || isCoVar tyvar, pprTyVar tyvar )
1900 zonkTyCoVarKind tyvar
1901
1902 zonkTyConBinders :: [TyConBinder] -> TcM [TyConBinder]
1903 zonkTyConBinders = mapM zonk1
1904 where
1905 zonk1 (Bndr tv vis)
1906 = do { tv' <- zonkTcTyCoVarBndr tv
1907 ; return (Bndr tv' vis) }
1908
1909 zonkTcTyVar :: TcTyVar -> TcM TcType
1910 -- Simply look through all Flexis
1911 zonkTcTyVar tv
1912 | isTcTyVar tv
1913 = case tcTyVarDetails tv of
1914 SkolemTv {} -> zonk_kind_and_return
1915 RuntimeUnk {} -> zonk_kind_and_return
1916 MetaTv { mtv_ref = ref }
1917 -> do { cts <- readMutVar ref
1918 ; case cts of
1919 Flexi -> zonk_kind_and_return
1920 Indirect ty -> do { zty <- zonkTcType ty
1921 ; writeTcRef ref (Indirect zty)
1922 -- See Note [Sharing in zonking]
1923 ; return zty } }
1924
1925 | otherwise -- coercion variable
1926 = zonk_kind_and_return
1927 where
1928 zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv
1929 ; return (mkTyVarTy z_tv) }
1930
1931 -- Variant that assumes that any result of zonking is still a TyVar.
1932 -- Should be used only on skolems and TyVarTvs
1933 zonkTcTyVarToTyVar :: HasDebugCallStack => TcTyVar -> TcM TcTyVar
1934 zonkTcTyVarToTyVar tv
1935 = do { ty <- zonkTcTyVar tv
1936 ; let tv' = case tcGetTyVar_maybe ty of
1937 Just tv' -> tv'
1938 Nothing -> pprPanic "zonkTcTyVarToTyVar"
1939 (ppr tv $$ ppr ty)
1940 ; return tv' }
1941
1942 zonkTyVarTyVarPairs :: [(Name,TcTyVar)] -> TcM [(Name,TcTyVar)]
1943 zonkTyVarTyVarPairs prs
1944 = mapM do_one prs
1945 where
1946 do_one (nm, tv) = do { tv' <- zonkTcTyVarToTyVar tv
1947 ; return (nm, tv') }
1948
1949 {- Note [Sharing in zonking]
1950 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1951 Suppose we have
1952 alpha :-> beta :-> gamma :-> ty
1953 where the ":->" means that the unification variable has been
1954 filled in with Indirect. Then when zonking alpha, it'd be nice
1955 to short-circuit beta too, so we end up with
1956 alpha :-> zty
1957 beta :-> zty
1958 gamma :-> zty
1959 where zty is the zonked version of ty. That way, if we come across
1960 beta later, we'll have less work to do. (And indeed the same for
1961 alpha.)
1962
1963 This is easily achieved: just overwrite (Indirect ty) with (Indirect
1964 zty). Non-systematic perf comparisons suggest that this is a modest
1965 win.
1966
1967 But c.f Note [Sharing when zonking to Type] in TcHsSyn.
1968
1969 %************************************************************************
1970 %* *
1971 Tidying
1972 * *
1973 ************************************************************************
1974 -}
1975
1976 zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
1977 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
1978 ; return (tidyOpenType env ty') }
1979
1980 zonkTidyTcTypes :: TidyEnv -> [TcType] -> TcM (TidyEnv, [TcType])
1981 zonkTidyTcTypes = zonkTidyTcTypes' []
1982 where zonkTidyTcTypes' zs env [] = return (env, reverse zs)
1983 zonkTidyTcTypes' zs env (ty:tys)
1984 = do { (env', ty') <- zonkTidyTcType env ty
1985 ; zonkTidyTcTypes' (ty':zs) env' tys }
1986
1987 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
1988 zonkTidyOrigin env (GivenOrigin skol_info)
1989 = do { skol_info1 <- zonkSkolemInfo skol_info
1990 ; let skol_info2 = tidySkolemInfo env skol_info1
1991 ; return (env, GivenOrigin skol_info2) }
1992 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act
1993 , uo_expected = exp })
1994 = do { (env1, act') <- zonkTidyTcType env act
1995 ; (env2, exp') <- zonkTidyTcType env1 exp
1996 ; return ( env2, orig { uo_actual = act'
1997 , uo_expected = exp' }) }
1998 zonkTidyOrigin env (KindEqOrigin ty1 m_ty2 orig t_or_k)
1999 = do { (env1, ty1') <- zonkTidyTcType env ty1
2000 ; (env2, m_ty2') <- case m_ty2 of
2001 Just ty2 -> second Just <$> zonkTidyTcType env1 ty2
2002 Nothing -> return (env1, Nothing)
2003 ; (env3, orig') <- zonkTidyOrigin env2 orig
2004 ; return (env3, KindEqOrigin ty1' m_ty2' orig' t_or_k) }
2005 zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
2006 = do { (env1, p1') <- zonkTidyTcType env p1
2007 ; (env2, p2') <- zonkTidyTcType env1 p2
2008 ; return (env2, FunDepOrigin1 p1' l1 p2' l2) }
2009 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
2010 = do { (env1, p1') <- zonkTidyTcType env p1
2011 ; (env2, p2') <- zonkTidyTcType env1 p2
2012 ; (env3, o1') <- zonkTidyOrigin env2 o1
2013 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
2014 zonkTidyOrigin env orig = return (env, orig)
2015
2016 ----------------
2017 tidyCt :: TidyEnv -> Ct -> Ct
2018 -- Used only in error reporting
2019 -- Also converts it to non-canonical
2020 tidyCt env ct
2021 = case ct of
2022 CHoleCan { cc_ev = ev }
2023 -> ct { cc_ev = tidy_ev env ev }
2024 _ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
2025 where
2026 tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
2027 -- NB: we do not tidy the ctev_evar field because we don't
2028 -- show it in error messages
2029 tidy_ev env ctev@(CtGiven { ctev_pred = pred })
2030 = ctev { ctev_pred = tidyType env pred }
2031 tidy_ev env ctev@(CtWanted { ctev_pred = pred })
2032 = ctev { ctev_pred = tidyType env pred }
2033 tidy_ev env ctev@(CtDerived { ctev_pred = pred })
2034 = ctev { ctev_pred = tidyType env pred }
2035
2036 ----------------
2037 tidyEvVar :: TidyEnv -> EvVar -> EvVar
2038 tidyEvVar env var = setVarType var (tidyType env (varType var))
2039
2040 ----------------
2041 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
2042 tidySkolemInfo env (DerivSkol ty) = DerivSkol (tidyType env ty)
2043 tidySkolemInfo env (SigSkol cx ty tv_prs) = tidySigSkol env cx ty tv_prs
2044 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
2045 tidySkolemInfo env (UnifyForAllSkol ty) = UnifyForAllSkol (tidyType env ty)
2046 tidySkolemInfo _ info = info
2047
2048 tidySigSkol :: TidyEnv -> UserTypeCtxt
2049 -> TcType -> [(Name,TcTyVar)] -> SkolemInfo
2050 -- We need to take special care when tidying SigSkol
2051 -- See Note [SigSkol SkolemInfo] in TcRnTypes
2052 tidySigSkol env cx ty tv_prs
2053 = SigSkol cx (tidy_ty env ty) tv_prs'
2054 where
2055 tv_prs' = mapSnd (tidyTyCoVarOcc env) tv_prs
2056 inst_env = mkNameEnv tv_prs'
2057
2058 tidy_ty env (ForAllTy (Bndr tv vis) ty)
2059 = ForAllTy (Bndr tv' vis) (tidy_ty env' ty)
2060 where
2061 (env', tv') = tidy_tv_bndr env tv
2062
2063 tidy_ty env (FunTy arg res)
2064 = FunTy (tidyType env arg) (tidy_ty env res)
2065
2066 tidy_ty env ty = tidyType env ty
2067
2068 tidy_tv_bndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
2069 tidy_tv_bndr env@(occ_env, subst) tv
2070 | Just tv' <- lookupNameEnv inst_env (tyVarName tv)
2071 = ((occ_env, extendVarEnv subst tv tv'), tv')
2072
2073 | otherwise
2074 = tidyVarBndr env tv
2075
2076 -------------------------------------------------------------------------
2077 {-
2078 %************************************************************************
2079 %* *
2080 Levity polymorphism checks
2081 * *
2082 ************************************************************************
2083
2084 See Note [Levity polymorphism checking] in DsMonad
2085
2086 -}
2087
2088 -- | According to the rules around representation polymorphism
2089 -- (see https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds), no binder
2090 -- can have a representation-polymorphic type. This check ensures
2091 -- that we respect this rule. It is a bit regrettable that this error
2092 -- occurs in zonking, after which we should have reported all errors.
2093 -- But it's hard to see where else to do it, because this can be discovered
2094 -- only after all solving is done. And, perhaps most importantly, this
2095 -- isn't really a compositional property of a type system, so it's
2096 -- not a terrible surprise that the check has to go in an awkward spot.
2097 ensureNotLevPoly :: Type -- its zonked type
2098 -> SDoc -- where this happened
2099 -> TcM ()
2100 ensureNotLevPoly ty doc
2101 = whenNoErrs $ -- sometimes we end up zonking bogus definitions of type
2102 -- forall a. a. See, for example, test ghci/scripts/T9140
2103 checkForLevPoly doc ty
2104
2105 -- See Note [Levity polymorphism checking] in DsMonad
2106 checkForLevPoly :: SDoc -> Type -> TcM ()
2107 checkForLevPoly = checkForLevPolyX addErr
2108
2109 checkForLevPolyX :: Monad m
2110 => (SDoc -> m ()) -- how to report an error
2111 -> SDoc -> Type -> m ()
2112 checkForLevPolyX add_err extra ty
2113 | isTypeLevPoly ty
2114 = add_err (formatLevPolyErr ty $$ extra)
2115 | otherwise
2116 = return ()
2117
2118 formatLevPolyErr :: Type -- levity-polymorphic type
2119 -> SDoc
2120 formatLevPolyErr ty
2121 = hang (text "A levity-polymorphic type is not allowed here:")
2122 2 (vcat [ text "Type:" <+> pprWithTYPE tidy_ty
2123 , text "Kind:" <+> pprWithTYPE tidy_ki ])
2124 where
2125 (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty
2126 tidy_ki = tidyType tidy_env (typeKind ty)