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