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