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