Make a smart mkAppTyM
[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_kind <- zonkTcType ty_kind
788 ; let kind_check_ok = tcIsConstraintKind zonked_tv_kind
789 || tcEqKind zonked_ty_kind zonked_tv_kind
790 -- Hack alert! tcIsConstraintKind: see TcHsType
791 -- Note [Extra-constraint holes in partial type signatures]
792
793 kind_msg = hang (text "Ill-kinded update to meta tyvar")
794 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
795 <+> text ":="
796 <+> ppr ty <+> text "::" <+> (ppr zonked_ty_kind) )
797
798 ; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
799
800 -- Check for double updates
801 ; MASSERT2( isFlexi meta_details, double_upd_msg meta_details )
802
803 -- Check for level OK
804 -- See Note [Level check when unifying]
805 ; MASSERT2( level_check_ok, level_check_msg )
806
807 -- Check Kinds ok
808 ; MASSERT2( kind_check_ok, kind_msg )
809
810 -- Do the write
811 ; writeMutVar ref (Indirect ty) }
812 where
813 tv_kind = tyVarKind tyvar
814 ty_kind = tcTypeKind ty
815
816 tv_lvl = tcTyVarLevel tyvar
817 ty_lvl = tcTypeLevel ty
818
819 level_check_ok = not (ty_lvl `strictlyDeeperThan` tv_lvl)
820 level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
821
822 double_upd_msg details = hang (text "Double update of meta tyvar")
823 2 (ppr tyvar $$ ppr details)
824
825 {- Note [Level check when unifying]
826 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
827 When unifying
828 alpha:lvl := ty
829 we expect that the TcLevel of 'ty' will be <= lvl.
830 However, during unflatting we do
831 fuv:l := ty:(l+1)
832 which is usually wrong; hence the check isFmmvTyVar in level_check_ok.
833 See Note [TcLevel assignment] in TcType.
834 -}
835
836 {-
837 % Generating fresh variables for pattern match check
838 -}
839
840
841 {-
842 ************************************************************************
843 * *
844 MetaTvs: TauTvs
845 * *
846 ************************************************************************
847
848 Note [Never need to instantiate coercion variables]
849 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
850 With coercion variables sloshing around in types, it might seem that we
851 sometimes need to instantiate coercion variables. This would be problematic,
852 because coercion variables inhabit unboxed equality (~#), and the constraint
853 solver thinks in terms only of boxed equality (~). The solution is that
854 we never need to instantiate coercion variables in the first place.
855
856 The tyvars that we need to instantiate come from the types of functions,
857 data constructors, and patterns. These will never be quantified over
858 coercion variables, except for the special case of the promoted Eq#. But,
859 that can't ever appear in user code, so we're safe!
860 -}
861
862 newTauTyVar :: Name -> Kind -> TcM TcTyVar
863 newTauTyVar name kind
864 = do { details <- newMetaDetails TauTv
865 ; let tyvar = mkTcTyVar name kind details
866 ; traceTc "newTauTyVar" (ppr tyvar)
867 ; return tyvar }
868
869
870 mkMetaTyVarName :: Unique -> FastString -> Name
871 -- Makes a /System/ Name, which is eagerly eliminated by
872 -- the unifier; see TcUnify.nicer_to_update_tv1, and
873 -- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
874 mkMetaTyVarName uniq str = mkSystemName uniq (mkTyVarOccFS str)
875
876 newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
877 -- Make a new meta tyvar out of thin air
878 newAnonMetaTyVar meta_info kind
879 = do { uniq <- newUnique
880 ; let name = mkMetaTyVarName uniq s
881 s = case meta_info of
882 TauTv -> fsLit "t"
883 FlatMetaTv -> fsLit "fmv"
884 FlatSkolTv -> fsLit "fsk"
885 TyVarTv -> fsLit "a"
886 ; details <- newMetaDetails meta_info
887 ; let tyvar = mkTcTyVar name kind details
888 ; traceTc "newAnonMetaTyVar" (ppr tyvar)
889 ; return tyvar }
890
891 cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
892 -- Same as newAnonMetaTyVar, but use a supplied TyVar as the source of the print-name
893 cloneAnonMetaTyVar info tv kind
894 = do { uniq <- newUnique
895 ; details <- newMetaDetails info
896 ; let name = mkSystemName uniq (getOccName tv)
897 -- See Note [Name of an instantiated type variable]
898 tyvar = mkTcTyVar name kind details
899 ; traceTc "cloneAnonMetaTyVar" (ppr tyvar)
900 ; return tyvar }
901
902 {- Note [Name of an instantiated type variable]
903 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
904 At the moment we give a unification variable a System Name, which
905 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
906 -}
907
908 newFlexiTyVar :: Kind -> TcM TcTyVar
909 newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
910
911 newFlexiTyVarTy :: Kind -> TcM TcType
912 newFlexiTyVarTy kind = do
913 tc_tyvar <- newFlexiTyVar kind
914 return (mkTyVarTy tc_tyvar)
915
916 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
917 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
918
919 newOpenTypeKind :: TcM TcKind
920 newOpenTypeKind
921 = do { rr <- newFlexiTyVarTy runtimeRepTy
922 ; return (tYPE rr) }
923
924 -- | Create a tyvar that can be a lifted or unlifted type.
925 -- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh
926 newOpenFlexiTyVarTy :: TcM TcType
927 newOpenFlexiTyVarTy
928 = do { kind <- newOpenTypeKind
929 ; newFlexiTyVarTy kind }
930
931 newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
932 -- Instantiate with META type variables
933 -- Note that this works for a sequence of kind, type, and coercion variables
934 -- variables. Eg [ (k:*), (a:k->k) ]
935 -- Gives [ (k7:*), (a8:k7->k7) ]
936 newMetaTyVars = newMetaTyVarsX emptyTCvSubst
937 -- emptyTCvSubst has an empty in-scope set, but that's fine here
938 -- Since the tyvars are freshly made, they cannot possibly be
939 -- captured by any existing for-alls.
940
941 newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
942 -- Just like newMetaTyVars, but start with an existing substitution.
943 newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
944
945 newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
946 -- Make a new unification variable tyvar whose Name and Kind come from
947 -- an existing TyVar. We substitute kind variables in the kind.
948 newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
949
950 newMetaTyVarTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
951 newMetaTyVarTyVars = mapAccumLM newMetaTyVarTyVarX emptyTCvSubst
952
953 newMetaTyVarTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
954 -- Just like newMetaTyVarX, but make a TyVarTv
955 newMetaTyVarTyVarX subst tyvar = new_meta_tv_x TyVarTv subst tyvar
956
957 newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
958 newWildCardX subst tv
959 = do { new_tv <- newAnonMetaTyVar TauTv (substTy subst (tyVarKind tv))
960 ; return (extendTvSubstWithClone subst tv new_tv, new_tv) }
961
962 new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
963 new_meta_tv_x info subst tv
964 = do { new_tv <- cloneAnonMetaTyVar info tv substd_kind
965 ; let subst1 = extendTvSubstWithClone subst tv new_tv
966 ; return (subst1, new_tv) }
967 where
968 substd_kind = substTyUnchecked subst (tyVarKind tv)
969 -- NOTE: Trac #12549 is fixed so we could use
970 -- substTy here, but the tc_infer_args problem
971 -- is not yet fixed so leaving as unchecked for now.
972 -- OLD NOTE:
973 -- Unchecked because we call newMetaTyVarX from
974 -- tcInstTyBinder, which is called from tcInferApps
975 -- which does not yet take enough trouble to ensure
976 -- the in-scope set is right; e.g. Trac #12785 trips
977 -- if we use substTy here
978
979 newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
980 newMetaTyVarTyAtLevel tc_lvl kind
981 = do { uniq <- newUnique
982 ; ref <- newMutVar Flexi
983 ; let name = mkMetaTyVarName uniq (fsLit "p")
984 details = MetaTv { mtv_info = TauTv
985 , mtv_ref = ref
986 , mtv_tclvl = tc_lvl }
987 ; return (mkTyVarTy (mkTcTyVar name kind details)) }
988
989 {- *********************************************************************
990 * *
991 Finding variables to quantify over
992 * *
993 ********************************************************************* -}
994
995 {- Note [Dependent type variables]
996 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
997 In Haskell type inference we quantify over type variables; but we only
998 quantify over /kind/ variables when -XPolyKinds is on. Without -XPolyKinds
999 we default the kind variables to *.
1000
1001 So, to support this defaulting, and only for that reason, when
1002 collecting the free vars of a type, prior to quantifying, we must keep
1003 the type and kind variables separate.
1004
1005 But what does that mean in a system where kind variables /are/ type
1006 variables? It's a fairly arbitrary distinction based on how the
1007 variables appear:
1008
1009 - "Kind variables" appear in the kind of some other free variable
1010
1011 These are the ones we default to * if -XPolyKinds is off
1012
1013 - "Type variables" are all free vars that are not kind variables
1014
1015 E.g. In the type T k (a::k)
1016 'k' is a kind variable, because it occurs in the kind of 'a',
1017 even though it also appears at "top level" of the type
1018 'a' is a type variable, because it doesn't
1019
1020 We gather these variables using a CandidatesQTvs record:
1021 DV { dv_kvs: Variables free in the kind of a free type variable
1022 or of a forall-bound type variable
1023 , dv_tvs: Variables sytactically free in the type }
1024
1025 So: dv_kvs are the kind variables of the type
1026 (dv_tvs - dv_kvs) are the type variable of the type
1027
1028 Note that
1029
1030 * A variable can occur in both.
1031 T k (x::k) The first occurrence of k makes it
1032 show up in dv_tvs, the second in dv_kvs
1033
1034 * We include any coercion variables in the "dependent",
1035 "kind-variable" set because we never quantify over them.
1036
1037 * The "kind variables" might depend on each other; e.g
1038 (k1 :: k2), (k2 :: *)
1039 The "type variables" do not depend on each other; if
1040 one did, it'd be classified as a kind variable!
1041
1042 Note [CandidatesQTvs determinism and order]
1043 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1044 * Determinism: when we quantify over type variables we decide the
1045 order in which they appear in the final type. Because the order of
1046 type variables in the type can end up in the interface file and
1047 affects some optimizations like worker-wrapper, we want this order to
1048 be deterministic.
1049
1050 To achieve that we use deterministic sets of variables that can be
1051 converted to lists in a deterministic order. For more information
1052 about deterministic sets see Note [Deterministic UniqFM] in UniqDFM.
1053
1054 * Order: as well as being deterministic, we use an
1055 accumulating-parameter style for candidateQTyVarsOfType so that we
1056 add variables one at a time, left to right. That means we tend to
1057 produce the variables in left-to-right order. This is just to make
1058 it bit more predicatable for the programmer.
1059
1060 Note [Naughty quantification candidates]
1061 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1062 Consider (#14880, dependent/should_compile/T14880-2), suppose
1063 we are trying to generalise this type:
1064
1065 forall arg. ... (alpha[tau]:arg) ...
1066
1067 We have a metavariable alpha whose kind mentions a skolem variable
1068 boudn inside the very type we are generalising.
1069 This can arise while type-checking a user-written type signature
1070 (see the test case for the full code).
1071
1072 We cannot generalise over alpha! That would produce a type like
1073 forall {a :: arg}. forall arg. ...blah...
1074 The fact that alpha's kind mentions arg renders it completely
1075 ineligible for generaliation.
1076
1077 However, we are not going to learn any new constraints on alpha,
1078 because its kind isn't even in scope in the outer context. So alpha
1079 is entirely unconstrained.
1080
1081 What then should we do with alpha? During generalization, every
1082 metavariable is either (A) promoted, (B) generalized, or (C) zapped
1083 (according again to Note [Recipe for checking a signature] in
1084 TcHsType).
1085
1086 * We can't generalise it.
1087 * We can't promote it, because its kind prevents that
1088 * We can't simply leave it be, because this type is about to
1089 go into the typing environment (as the type of some let-bound
1090 variable, say), and then chaos erupts when we try to instantiate.
1091
1092 So, we zap it, eagerly, to Any. We don't have to do this eager zapping
1093 in terms (say, in `length []`) because terms are never re-examined before
1094 the final zonk (which zaps any lingering metavariables to Any).
1095
1096 We do this eager zapping in candidateQTyVars, which always precedes
1097 generalisation, because at that moment we have a clear picture of
1098 what skolems are in scope.
1099
1100 -}
1101
1102 data CandidatesQTvs
1103 -- See Note [Dependent type variables]
1104 -- See Note [CandidatesQTvs determinism and order]
1105 --
1106 -- Invariants:
1107 -- * All variables stored here are MetaTvs. No exceptions.
1108 -- * All variables are fully zonked, including their kinds
1109 --
1110 = DV { dv_kvs :: DTyVarSet -- "kind" metavariables (dependent)
1111 , dv_tvs :: DTyVarSet -- "type" metavariables (non-dependent)
1112 -- A variable may appear in both sets
1113 -- E.g. T k (x::k) The first occurrence of k makes it
1114 -- show up in dv_tvs, the second in dv_kvs
1115 -- See Note [Dependent type variables]
1116
1117 , dv_cvs :: CoVarSet
1118 -- These are covars. We will *not* quantify over these, but
1119 -- we must make sure also not to quantify over any cv's kinds,
1120 -- so we include them here as further direction for quantifyTyVars
1121 }
1122
1123 instance Semi.Semigroup CandidatesQTvs where
1124 (DV { dv_kvs = kv1, dv_tvs = tv1, dv_cvs = cv1 })
1125 <> (DV { dv_kvs = kv2, dv_tvs = tv2, dv_cvs = cv2 })
1126 = DV { dv_kvs = kv1 `unionDVarSet` kv2
1127 , dv_tvs = tv1 `unionDVarSet` tv2
1128 , dv_cvs = cv1 `unionVarSet` cv2 }
1129
1130 instance Monoid CandidatesQTvs where
1131 mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet, dv_cvs = emptyVarSet }
1132 mappend = (Semi.<>)
1133
1134 instance Outputable CandidatesQTvs where
1135 ppr (DV {dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs })
1136 = text "DV" <+> braces (pprWithCommas id [ text "dv_kvs =" <+> ppr kvs
1137 , text "dv_tvs =" <+> ppr tvs
1138 , text "dv_cvs =" <+> ppr cvs ])
1139
1140
1141 candidateKindVars :: CandidatesQTvs -> TyVarSet
1142 candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs)
1143
1144 -- | Gathers free variables to use as quantification candidates (in
1145 -- 'quantifyTyVars'). This might output the same var
1146 -- in both sets, if it's used in both a type and a kind.
1147 -- See Note [CandidatesQTvs determinism and order]
1148 -- See Note [Dependent type variables]
1149 candidateQTyVarsOfType :: TcType -- not necessarily zonked
1150 -> TcM CandidatesQTvs
1151 candidateQTyVarsOfType ty = collect_cand_qtvs False emptyVarSet mempty ty
1152
1153 -- | Like 'splitDepVarsOfType', but over a list of types
1154 candidateQTyVarsOfTypes :: [Type] -> TcM CandidatesQTvs
1155 candidateQTyVarsOfTypes tys = foldlM (collect_cand_qtvs False emptyVarSet) mempty tys
1156
1157 -- | Like 'candidateQTyVarsOfType', but consider every free variable
1158 -- to be dependent. This is appropriate when generalizing a *kind*,
1159 -- instead of a type. (That way, -XNoPolyKinds will default the variables
1160 -- to Type.)
1161 candidateQTyVarsOfKind :: TcKind -- Not necessarily zonked
1162 -> TcM CandidatesQTvs
1163 candidateQTyVarsOfKind ty = collect_cand_qtvs True emptyVarSet mempty ty
1164
1165 candidateQTyVarsOfKinds :: [TcKind] -- Not necessarily zonked
1166 -> TcM CandidatesQTvs
1167 candidateQTyVarsOfKinds tys = foldM (collect_cand_qtvs True emptyVarSet) mempty tys
1168
1169 delCandidates :: CandidatesQTvs -> [Var] -> CandidatesQTvs
1170 delCandidates (DV { dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) vars
1171 = DV { dv_kvs = kvs `delDVarSetList` vars
1172 , dv_tvs = tvs `delDVarSetList` vars
1173 , dv_cvs = cvs `delVarSetList` vars }
1174
1175 collect_cand_qtvs
1176 :: Bool -- True <=> consider every fv in Type to be dependent
1177 -> VarSet -- Bound variables (both locally bound and globally bound)
1178 -> CandidatesQTvs -- Accumulating parameter
1179 -> Type -- Not necessarily zonked
1180 -> TcM CandidatesQTvs
1181
1182 -- Key points:
1183 -- * Looks through meta-tyvars as it goes;
1184 -- no need to zonk in advance
1185 --
1186 -- * Needs to be monadic anyway, because it does the zap-naughty
1187 -- stuff; see Note [Naughty quantification candidates]
1188 --
1189 -- * Returns fully-zonked CandidateQTvs, including their kinds
1190 -- so that subsequent dependency analysis (to build a well
1191 -- scoped telescope) works correctly
1192
1193 collect_cand_qtvs is_dep bound dvs ty
1194 = go dvs ty
1195 where
1196 is_bound tv = tv `elemVarSet` bound
1197
1198 -----------------
1199 go :: CandidatesQTvs -> TcType -> TcM CandidatesQTvs
1200 -- Uses accumulating-parameter style
1201 go dv (AppTy t1 t2) = foldlM go dv [t1, t2]
1202 go dv (TyConApp _ tys) = foldlM go dv tys
1203 go dv (FunTy arg res) = foldlM go dv [arg, res]
1204 go dv (LitTy {}) = return dv
1205 go dv (CastTy ty co) = do dv1 <- go dv ty
1206 collect_cand_qtvs_co bound dv1 co
1207 go dv (CoercionTy co) = collect_cand_qtvs_co bound dv co
1208
1209 go dv (TyVarTy tv)
1210 | is_bound tv = return dv
1211 | otherwise = do { m_contents <- isFilledMetaTyVar_maybe tv
1212 ; case m_contents of
1213 Just ind_ty -> go dv ind_ty
1214 Nothing -> go_tv dv tv }
1215
1216 go dv (ForAllTy (Bndr tv _) ty)
1217 = do { dv1 <- collect_cand_qtvs True bound dv (tyVarKind tv)
1218 ; collect_cand_qtvs is_dep (bound `extendVarSet` tv) dv1 ty }
1219
1220 -----------------
1221 go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv
1222 | tv `elemDVarSet` kvs = return dv -- We have met this tyvar aleady
1223 | not is_dep
1224 , tv `elemDVarSet` tvs = return dv -- We have met this tyvar aleady
1225 | otherwise
1226 = do { tv_kind <- zonkTcType (tyVarKind tv)
1227 -- This zonk is annoying, but it is necessary, both to
1228 -- ensure that the collected candidates have zonked kinds
1229 -- (Trac #15795) and to make the naughty check
1230 -- (which comes next) works correctly
1231 ; if intersectsVarSet bound (tyCoVarsOfType tv_kind)
1232
1233 then -- See Note [Naughty quantification candidates]
1234 do { traceTc "Zapping naughty quantifier" (pprTyVar tv)
1235 ; writeMetaTyVar tv (anyTypeOfKind tv_kind)
1236 ; collect_cand_qtvs True bound dv tv_kind }
1237
1238 else do { let tv' = tv `setTyVarKind` tv_kind
1239 dv' | is_dep = dv { dv_kvs = kvs `extendDVarSet` tv' }
1240 | otherwise = dv { dv_tvs = tvs `extendDVarSet` tv' }
1241 -- See Note [Order of accumulation]
1242 ; collect_cand_qtvs True emptyVarSet dv' tv_kind } }
1243
1244 collect_cand_qtvs_co :: VarSet -- bound variables
1245 -> CandidatesQTvs -> Coercion
1246 -> TcM CandidatesQTvs
1247 collect_cand_qtvs_co bound = go_co
1248 where
1249 go_co dv (Refl ty) = collect_cand_qtvs True bound dv ty
1250 go_co dv (GRefl _ ty mco) = do dv1 <- collect_cand_qtvs True bound dv ty
1251 go_mco dv1 mco
1252 go_co dv (TyConAppCo _ _ cos) = foldlM go_co dv cos
1253 go_co dv (AppCo co1 co2) = foldlM go_co dv [co1, co2]
1254 go_co dv (FunCo _ co1 co2) = foldlM go_co dv [co1, co2]
1255 go_co dv (AxiomInstCo _ _ cos) = foldlM go_co dv cos
1256 go_co dv (AxiomRuleCo _ cos) = foldlM go_co dv cos
1257 go_co dv (UnivCo prov _ t1 t2) = do dv1 <- go_prov dv prov
1258 dv2 <- collect_cand_qtvs True bound dv1 t1
1259 collect_cand_qtvs True bound dv2 t2
1260 go_co dv (SymCo co) = go_co dv co
1261 go_co dv (TransCo co1 co2) = foldlM go_co dv [co1, co2]
1262 go_co dv (NthCo _ _ co) = go_co dv co
1263 go_co dv (LRCo _ co) = go_co dv co
1264 go_co dv (InstCo co1 co2) = foldlM go_co dv [co1, co2]
1265 go_co dv (KindCo co) = go_co dv co
1266 go_co dv (SubCo co) = go_co dv co
1267
1268 go_co dv (HoleCo hole) = do m_co <- unpackCoercionHole_maybe hole
1269 case m_co of
1270 Just co -> go_co dv co
1271 Nothing -> go_cv dv (coHoleCoVar hole)
1272
1273 go_co dv (CoVarCo cv) = go_cv dv cv
1274
1275 go_co dv (ForAllCo tcv kind_co co)
1276 = do { dv1 <- go_co dv kind_co
1277 ; collect_cand_qtvs_co (bound `extendVarSet` tcv) dv1 co }
1278
1279 go_mco dv MRefl = return dv
1280 go_mco dv (MCo co) = go_co dv co
1281
1282 go_prov dv UnsafeCoerceProv = return dv
1283 go_prov dv (PhantomProv co) = go_co dv co
1284 go_prov dv (ProofIrrelProv co) = go_co dv co
1285 go_prov dv (PluginProv _) = return dv
1286
1287 go_cv :: CandidatesQTvs -> CoVar -> TcM CandidatesQTvs
1288 go_cv dv@(DV { dv_cvs = cvs }) cv
1289 | is_bound cv = return dv
1290 | cv `elemVarSet` cvs = return dv
1291 | otherwise = collect_cand_qtvs True emptyVarSet
1292 (dv { dv_cvs = cvs `extendVarSet` cv })
1293 (idType cv)
1294
1295 is_bound tv = tv `elemVarSet` bound
1296
1297 {- Note [Order of accumulation]
1298 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1299 You might be tempted (like I was) to use unitDVarSet and mappend
1300 rather than extendDVarSet. However, the union algorithm for
1301 deterministic sets depends on (roughly) the size of the sets. The
1302 elements from the smaller set end up to the right of the elements from
1303 the larger one. When sets are equal, the left-hand argument to
1304 `mappend` goes to the right of the right-hand argument.
1305
1306 In our case, if we use unitDVarSet and mappend, we learn that the free
1307 variables of (a -> b -> c -> d) are [b, a, c, d], and we then quantify
1308 over them in that order. (The a comes after the b because we union the
1309 singleton sets as ({a} `mappend` {b}), producing {b, a}. Thereafter,
1310 the size criterion works to our advantage.) This is just annoying to
1311 users, so I use `extendDVarSet`, which unambiguously puts the new
1312 element to the right.
1313
1314 Note that the unitDVarSet/mappend implementation would not be wrong
1315 against any specification -- just suboptimal and confounding to users.
1316 -}
1317
1318 {- *********************************************************************
1319 * *
1320 Quantification
1321 * *
1322 ************************************************************************
1323
1324 Note [quantifyTyVars]
1325 ~~~~~~~~~~~~~~~~~~~~~
1326 quantifyTyVars is given the free vars of a type that we
1327 are about to wrap in a forall.
1328
1329 It takes these free type/kind variables (partitioned into dependent and
1330 non-dependent variables) and
1331 1. Zonks them and remove globals and covars
1332 2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
1333 3. Calls skolemiseQuantifiedTyVar on each
1334
1335 Step (2) is often unimportant, because the kind variable is often
1336 also free in the type. Eg
1337 Typeable k (a::k)
1338 has free vars {k,a}. But the type (see Trac #7916)
1339 (f::k->*) (a::k)
1340 has free vars {f,a}, but we must add 'k' as well! Hence step (2).
1341
1342 * This function distinguishes between dependent and non-dependent
1343 variables only to keep correct defaulting behavior with -XNoPolyKinds.
1344 With -XPolyKinds, it treats both classes of variables identically.
1345
1346 * quantifyTyVars never quantifies over
1347 - a coercion variable (or any tv mentioned in the kind of a covar)
1348 - a runtime-rep variable
1349
1350 Note [quantifyTyVars determinism]
1351 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1352 The results of quantifyTyVars are wrapped in a forall and can end up in the
1353 interface file. One such example is inferred type signatures. They also affect
1354 the results of optimizations, for example worker-wrapper. This means that to
1355 get deterministic builds quantifyTyVars needs to be deterministic.
1356
1357 To achieve this CandidatesQTvs is backed by deterministic sets which allows them
1358 to be later converted to a list in a deterministic order.
1359
1360 For more information about deterministic sets see
1361 Note [Deterministic UniqFM] in UniqDFM.
1362 -}
1363
1364 quantifyTyVars
1365 :: TcTyCoVarSet -- Global tvs; already zonked
1366 -> CandidatesQTvs -- See Note [Dependent type variables]
1367 -- Already zonked
1368 -> TcM [TcTyVar]
1369 -- See Note [quantifyTyVars]
1370 -- Can be given a mixture of TcTyVars and TyVars, in the case of
1371 -- associated type declarations. Also accepts covars, but *never* returns any.
1372 quantifyTyVars gbl_tvs
1373 dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs, dv_cvs = covars })
1374 = do { outer_tclvl <- getTcLevel
1375 ; traceTc "quantifyTyVars 1" (vcat [ppr outer_tclvl, ppr dvs, ppr gbl_tvs])
1376 ; let co_tvs = closeOverKinds covars
1377 mono_tvs = gbl_tvs `unionVarSet` co_tvs
1378 -- NB: All variables in the kind of a covar must not be
1379 -- quantified over, as we don't quantify over the covar.
1380
1381 dep_kvs = dVarSetElemsWellScoped $
1382 dep_tkvs `dVarSetMinusVarSet` mono_tvs
1383 -- dVarSetElemsWellScoped: put the kind variables into
1384 -- well-scoped order.
1385 -- E.g. [k, (a::k)] not the other way roud
1386
1387 nondep_tvs = dVarSetElems $
1388 (nondep_tkvs `minusDVarSet` dep_tkvs)
1389 `dVarSetMinusVarSet` mono_tvs
1390 -- See Note [Dependent type variables]
1391 -- The `minus` dep_tkvs removes any kind-level vars
1392 -- e.g. T k (a::k) Since k appear in a kind it'll
1393 -- be in dv_kvs, and is dependent. So remove it from
1394 -- dv_tvs which will also contain k
1395 -- No worry about dependent covars here;
1396 -- they are all in dep_tkvs
1397 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
1398
1399 -- This block uses level numbers to decide what to quantify
1400 -- and emits a warning if the two methods do not give the same answer
1401 ; let dep_kvs2 = dVarSetElemsWellScoped $
1402 filterDVarSet (quantifiableTv outer_tclvl) dep_tkvs
1403 nondep_tvs2 = filter (quantifiableTv outer_tclvl) $
1404 dVarSetElems (nondep_tkvs `minusDVarSet` dep_tkvs)
1405
1406 all_ok = dep_kvs == dep_kvs2 && nondep_tvs == nondep_tvs2
1407 bad_msg = hang (text "Quantification by level numbers would fail")
1408 2 (vcat [ text "Outer level =" <+> ppr outer_tclvl
1409 , text "dep_tkvs =" <+> ppr dep_tkvs
1410 , text "co_vars =" <+> vcat [ ppr cv <+> dcolon <+> ppr (varType cv)
1411 | cv <- nonDetEltsUniqSet covars ]
1412 , text "co_tvs =" <+> ppr co_tvs
1413 , text "dep_kvs =" <+> ppr dep_kvs
1414 , text "dep_kvs2 =" <+> ppr dep_kvs2
1415 , text "nondep_tvs =" <+> ppr nondep_tvs
1416 , text "nondep_tvs2 =" <+> ppr nondep_tvs2 ])
1417 ; WARN( not all_ok, bad_msg ) return ()
1418
1419 -- In the non-PolyKinds case, default the kind variables
1420 -- to *, and zonk the tyvars as usual. Notice that this
1421 -- may make quantifyTyVars return a shorter list
1422 -- than it was passed, but that's ok
1423 ; poly_kinds <- xoptM LangExt.PolyKinds
1424 ; dep_kvs' <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs
1425 ; nondep_tvs' <- mapMaybeM (zonk_quant False) nondep_tvs
1426 ; let final_qtvs = dep_kvs' ++ nondep_tvs'
1427 -- Because of the order, any kind variables
1428 -- mentioned in the kinds of the nondep_tvs'
1429 -- now refer to the dep_kvs'
1430
1431 ; traceTc "quantifyTyVars 2"
1432 (vcat [ text "globals:" <+> ppr gbl_tvs
1433 , text "mono_tvs:" <+> ppr mono_tvs
1434 , text "nondep:" <+> pprTyVars nondep_tvs
1435 , text "dep:" <+> pprTyVars dep_kvs
1436 , text "dep_kvs'" <+> pprTyVars dep_kvs'
1437 , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ])
1438
1439 -- We should never quantify over coercion variables; check this
1440 ; let co_vars = filter isCoVar final_qtvs
1441 ; MASSERT2( null co_vars, ppr co_vars )
1442
1443 ; return final_qtvs }
1444 where
1445 -- zonk_quant returns a tyvar if it should be quantified over;
1446 -- otherwise, it returns Nothing. The latter case happens for
1447 -- * Kind variables, with -XNoPolyKinds: don't quantify over these
1448 -- * RuntimeRep variables: we never quantify over these
1449 zonk_quant default_kind tkv
1450 | not (isTyVar tkv)
1451 = return Nothing -- this can happen for a covar that's associated with
1452 -- a coercion hole. Test case: typecheck/should_compile/T2494
1453
1454 | not (isTcTyVar tkv) -- I don't think this can ever happen.
1455 -- Hence the assert
1456 = ASSERT2( False, text "quantifying over a TyVar" <+> ppr tkv)
1457 return (Just tkv)
1458
1459 | otherwise
1460 = do { deflt_done <- defaultTyVar default_kind tkv
1461 ; case deflt_done of
1462 True -> return Nothing
1463 False -> do { tv <- skolemiseQuantifiedTyVar tkv
1464 ; return (Just tv) } }
1465
1466 quantifiableTv :: TcLevel -- Level of the context, outside the quantification
1467 -> TcTyVar
1468 -> Bool
1469 quantifiableTv outer_tclvl tcv
1470 | isTcTyVar tcv -- Might be a CoVar; change this when gather covars separtely
1471 = tcTyVarLevel tcv > outer_tclvl
1472 | otherwise
1473 = False
1474
1475 skolemiseQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
1476 -- The quantified type variables often include meta type variables
1477 -- we want to freeze them into ordinary type variables
1478 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
1479 -- bound occurrences of the original type variable will get zonked to
1480 -- the immutable version.
1481 --
1482 -- We leave skolem TyVars alone; they are immutable.
1483 --
1484 -- This function is called on both kind and type variables,
1485 -- but kind variables *only* if PolyKinds is on.
1486
1487 skolemiseQuantifiedTyVar tv
1488 = case tcTyVarDetails tv of
1489 SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
1490 ; return (setTyVarKind tv kind) }
1491 -- It might be a skolem type variable,
1492 -- for example from a user type signature
1493
1494 MetaTv {} -> skolemiseUnboundMetaTyVar tv
1495
1496 _other -> pprPanic "skolemiseQuantifiedTyVar" (ppr tv) -- RuntimeUnk
1497
1498 defaultTyVar :: Bool -- True <=> please default this kind variable to *
1499 -> TcTyVar -- If it's a MetaTyVar then it is unbound
1500 -> TcM Bool -- True <=> defaulted away altogether
1501
1502 defaultTyVar default_kind tv
1503 | not (isMetaTyVar tv)
1504 = return False
1505
1506 | isTyVarTyVar tv
1507 -- Do not default TyVarTvs. Doing so would violate the invariants
1508 -- on TyVarTvs; see Note [Signature skolems] in TcType.
1509 -- Trac #13343 is an example; #14555 is another
1510 -- See Note [Inferring kinds for type declarations] in TcTyClsDecls
1511 = return False
1512
1513
1514 | isRuntimeRepVar tv -- Do not quantify over a RuntimeRep var
1515 -- unless it is a TyVarTv, handled earlier
1516 = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
1517 ; writeMetaTyVar tv liftedRepTy
1518 ; return True }
1519
1520 | default_kind -- -XNoPolyKinds and this is a kind var
1521 = default_kind_var tv -- so default it to * if possible
1522
1523 | otherwise
1524 = return False
1525
1526 where
1527 default_kind_var :: TyVar -> TcM Bool
1528 -- defaultKindVar is used exclusively with -XNoPolyKinds
1529 -- See Note [Defaulting with -XNoPolyKinds]
1530 -- It takes an (unconstrained) meta tyvar and defaults it.
1531 -- Works only on vars of type *; for other kinds, it issues an error.
1532 default_kind_var kv
1533 | isLiftedTypeKind (tyVarKind kv)
1534 = do { traceTc "Defaulting a kind var to *" (ppr kv)
1535 ; writeMetaTyVar kv liftedTypeKind
1536 ; return True }
1537 | otherwise
1538 = do { addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
1539 , text "of kind:" <+> ppr (tyVarKind kv')
1540 , text "Perhaps enable PolyKinds or add a kind signature" ])
1541 -- We failed to default it, so return False to say so.
1542 -- Hence, it'll get skolemised. That might seem odd, but we must either
1543 -- promote, skolemise, or zap-to-Any, to satisfy TcHsType
1544 -- Note [Recipe for checking a signature]
1545 -- Otherwise we get level-number assertion failures. It doesn't matter much
1546 -- because we are in an error siutation anyway.
1547 ; return False
1548 }
1549 where
1550 (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
1551
1552 skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar
1553 -- We have a Meta tyvar with a ref-cell inside it
1554 -- Skolemise it, so that we are totally out of Meta-tyvar-land
1555 -- We create a skolem TcTyVar, not a regular TyVar
1556 -- See Note [Zonking to Skolem]
1557 skolemiseUnboundMetaTyVar tv
1558 = ASSERT2( isMetaTyVar tv, ppr tv )
1559 do { when debugIsOn (check_empty tv)
1560 ; span <- getSrcSpanM -- Get the location from "here"
1561 -- ie where we are generalising
1562 ; kind <- zonkTcType (tyVarKind tv)
1563 ; let uniq = getUnique tv
1564 -- NB: Use same Unique as original tyvar. This is
1565 -- convenient in reading dumps, but is otherwise inessential.
1566
1567 tv_name = getOccName tv
1568 final_name = mkInternalName uniq tv_name span
1569 final_tv = mkTcTyVar final_name kind details
1570
1571 ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
1572 ; writeMetaTyVar tv (mkTyVarTy final_tv)
1573 ; return final_tv }
1574
1575 where
1576 details = SkolemTv (metaTyVarTcLevel tv) False
1577 check_empty tv -- [Sept 04] Check for non-empty.
1578 = when debugIsOn $ -- See note [Silly Type Synonym]
1579 do { cts <- readMetaTyVar tv
1580 ; case cts of
1581 Flexi -> return ()
1582 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
1583 return () }
1584
1585 {- Note [Defaulting with -XNoPolyKinds]
1586 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1587 Consider
1588
1589 data Compose f g a = Mk (f (g a))
1590
1591 We infer
1592
1593 Compose :: forall k1 k2. (k2 -> *) -> (k1 -> k2) -> k1 -> *
1594 Mk :: forall k1 k2 (f :: k2 -> *) (g :: k1 -> k2) (a :: k1).
1595 f (g a) -> Compose k1 k2 f g a
1596
1597 Now, in another module, we have -XNoPolyKinds -XDataKinds in effect.
1598 What does 'Mk mean? Pre GHC-8.0 with -XNoPolyKinds,
1599 we just defaulted all kind variables to *. But that's no good here,
1600 because the kind variables in 'Mk aren't of kind *, so defaulting to *
1601 is ill-kinded.
1602
1603 After some debate on #11334, we decided to issue an error in this case.
1604 The code is in defaultKindVar.
1605
1606 Note [What is a meta variable?]
1607 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1608 A "meta type-variable", also know as a "unification variable" is a placeholder
1609 introduced by the typechecker for an as-yet-unknown monotype.
1610
1611 For example, when we see a call `reverse (f xs)`, we know that we calling
1612 reverse :: forall a. [a] -> [a]
1613 So we know that the argument `f xs` must be a "list of something". But what is
1614 the "something"? We don't know until we explore the `f xs` a bit more. So we set
1615 out what we do know at the call of `reverse` by instantiate its type with a fresh
1616 meta tyvar, `alpha` say. So now the type of the argument `f xs`, and of the
1617 result, is `[alpha]`. The unification variable `alpha` stands for the
1618 as-yet-unknown type of the elements of the list.
1619
1620 As type inference progresses we may learn more about `alpha`. For example, suppose
1621 `f` has the type
1622 f :: forall b. b -> [Maybe b]
1623 Then we instantiate `f`'s type with another fresh unification variable, say
1624 `beta`; and equate `f`'s result type with reverse's argument type, thus
1625 `[alpha] ~ [Maybe beta]`.
1626
1627 Now we can solve this equality to learn that `alpha ~ Maybe beta`, so we've
1628 refined our knowledge about `alpha`. And so on.
1629
1630 If you found this Note useful, you may also want to have a look at
1631 Section 5 of "Practical type inference for higher rank types" (Peyton Jones,
1632 Vytiniotis, Weirich and Shields. J. Functional Programming. 2011).
1633
1634 Note [What is zonking?]
1635 ~~~~~~~~~~~~~~~~~~~~~~~
1636 GHC relies heavily on mutability in the typechecker for efficient operation.
1637 For this reason, throughout much of the type checking process meta type
1638 variables (the MetaTv constructor of TcTyVarDetails) are represented by mutable
1639 variables (known as TcRefs).
1640
1641 Zonking is the process of ripping out these mutable variables and replacing them
1642 with a real Type. This involves traversing the entire type expression, but the
1643 interesting part of replacing the mutable variables occurs in zonkTyVarOcc.
1644
1645 There are two ways to zonk a Type:
1646
1647 * zonkTcTypeToType, which is intended to be used at the end of type-checking
1648 for the final zonk. It has to deal with unfilled metavars, either by filling
1649 it with a value like Any or failing (determined by the UnboundTyVarZonker
1650 used).
1651
1652 * zonkTcType, which will happily ignore unfilled metavars. This is the
1653 appropriate function to use while in the middle of type-checking.
1654
1655 Note [Zonking to Skolem]
1656 ~~~~~~~~~~~~~~~~~~~~~~~~
1657 We used to zonk quantified type variables to regular TyVars. However, this
1658 leads to problems. Consider this program from the regression test suite:
1659
1660 eval :: Int -> String -> String -> String
1661 eval 0 root actual = evalRHS 0 root actual
1662
1663 evalRHS :: Int -> a
1664 evalRHS 0 root actual = eval 0 root actual
1665
1666 It leads to the deferral of an equality (wrapped in an implication constraint)
1667
1668 forall a. () => ((String -> String -> String) ~ a)
1669
1670 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
1671 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
1672 This has the *side effect* of also zonking the `a' in the deferred equality
1673 (which at this point is being handed around wrapped in an implication
1674 constraint).
1675
1676 Finally, the equality (with the zonked `a') will be handed back to the
1677 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
1678 If we zonk `a' with a regular type variable, we will have this regular type
1679 variable now floating around in the simplifier, which in many places assumes to
1680 only see proper TcTyVars.
1681
1682 We can avoid this problem by zonking with a skolem. The skolem is rigid
1683 (which we require for a quantified variable), but is still a TcTyVar that the
1684 simplifier knows how to deal with.
1685
1686 Note [Silly Type Synonyms]
1687 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1688 Consider this:
1689 type C u a = u -- Note 'a' unused
1690
1691 foo :: (forall a. C u a -> C u a) -> u
1692 foo x = ...
1693
1694 bar :: Num u => u
1695 bar = foo (\t -> t + t)
1696
1697 * From the (\t -> t+t) we get type {Num d} => d -> d
1698 where d is fresh.
1699
1700 * Now unify with type of foo's arg, and we get:
1701 {Num (C d a)} => C d a -> C d a
1702 where a is fresh.
1703
1704 * Now abstract over the 'a', but float out the Num (C d a) constraint
1705 because it does not 'really' mention a. (see exactTyVarsOfType)
1706 The arg to foo becomes
1707 \/\a -> \t -> t+t
1708
1709 * So we get a dict binding for Num (C d a), which is zonked to give
1710 a = ()
1711 [Note Sept 04: now that we are zonking quantified type variables
1712 on construction, the 'a' will be frozen as a regular tyvar on
1713 quantification, so the floated dict will still have type (C d a).
1714 Which renders this whole note moot; happily!]
1715
1716 * Then the \/\a abstraction has a zonked 'a' in it.
1717
1718 All very silly. I think its harmless to ignore the problem. We'll end up with
1719 a \/\a in the final result but all the occurrences of a will be zonked to ()
1720
1721 ************************************************************************
1722 * *
1723 Zonking types
1724 * *
1725 ************************************************************************
1726
1727 -}
1728
1729 -- | @tcGetGlobalTyCoVars@ returns a fully-zonked set of *scoped* tyvars free in
1730 -- the environment. To improve subsequent calls to the same function it writes
1731 -- the zonked set back into the environment. Note that this returns all
1732 -- variables free in anything (term-level or type-level) in scope. We thus
1733 -- don't have to worry about clashes with things that are not in scope, because
1734 -- if they are reachable, then they'll be returned here.
1735 -- NB: This is closed over kinds, so it can return unification variables mentioned
1736 -- in the kinds of in-scope tyvars.
1737 tcGetGlobalTyCoVars :: TcM TcTyVarSet
1738 tcGetGlobalTyCoVars
1739 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
1740 ; gbl_tvs <- readMutVar gtv_var
1741 ; gbl_tvs' <- zonkTyCoVarsAndFV gbl_tvs
1742 ; writeMutVar gtv_var gbl_tvs'
1743 ; return gbl_tvs' }
1744
1745 zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
1746 -- Zonk a type and take its free variables
1747 -- With kind polymorphism it can be essential to zonk *first*
1748 -- so that we find the right set of free variables. Eg
1749 -- forall k1. forall (a:k2). a
1750 -- where k2:=k1 is in the substitution. We don't want
1751 -- k2 to look free in this type!
1752 zonkTcTypeAndFV ty
1753 = tyCoVarsOfTypeDSet <$> zonkTcType ty
1754
1755 zonkTyCoVar :: TyCoVar -> TcM TcType
1756 -- Works on TyVars and TcTyVars
1757 zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
1758 | isTyVar tv = mkTyVarTy <$> zonkTyCoVarKind tv
1759 | otherwise = ASSERT2( isCoVar tv, ppr tv )
1760 mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
1761 -- Hackily, when typechecking type and class decls
1762 -- we have TyVars in scope added (only) in
1763 -- TcHsType.bindTyClTyVars, but it seems
1764 -- painful to make them into TcTyVars there
1765
1766 zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
1767 zonkTyCoVarsAndFV tycovars
1768 = tyCoVarsOfTypes <$> mapM zonkTyCoVar (nonDetEltsUniqSet tycovars)
1769 -- It's OK to use nonDetEltsUniqSet here because we immediately forget about
1770 -- the ordering by turning it into a nondeterministic set and the order
1771 -- of zonking doesn't matter for determinism.
1772
1773 -- Takes a list of TyCoVars, zonks them and returns a
1774 -- deterministically ordered list of their free variables.
1775 zonkTyCoVarsAndFVList :: [TyCoVar] -> TcM [TyCoVar]
1776 zonkTyCoVarsAndFVList tycovars
1777 = tyCoVarsOfTypesList <$> mapM zonkTyCoVar tycovars
1778
1779 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
1780 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
1781
1782 ----------------- Types
1783 zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
1784 zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
1785 ; return (setTyVarKind tv kind') }
1786
1787 zonkTcTypes :: [TcType] -> TcM [TcType]
1788 zonkTcTypes tys = mapM zonkTcType tys
1789
1790 {-
1791 ************************************************************************
1792 * *
1793 Zonking constraints
1794 * *
1795 ************************************************************************
1796 -}
1797
1798 zonkImplication :: Implication -> TcM Implication
1799 zonkImplication implic@(Implic { ic_skols = skols
1800 , ic_given = given
1801 , ic_wanted = wanted
1802 , ic_info = info })
1803 = do { skols' <- mapM zonkTyCoVarKind skols -- Need to zonk their kinds!
1804 -- as Trac #7230 showed
1805 ; given' <- mapM zonkEvVar given
1806 ; info' <- zonkSkolemInfo info
1807 ; wanted' <- zonkWCRec wanted
1808 ; return (implic { ic_skols = skols'
1809 , ic_given = given'
1810 , ic_wanted = wanted'
1811 , ic_info = info' }) }
1812
1813 zonkEvVar :: EvVar -> TcM EvVar
1814 zonkEvVar var = do { ty' <- zonkTcType (varType var)
1815 ; return (setVarType var ty') }
1816
1817
1818 zonkWC :: WantedConstraints -> TcM WantedConstraints
1819 zonkWC wc = zonkWCRec wc
1820
1821 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
1822 zonkWCRec (WC { wc_simple = simple, wc_impl = implic })
1823 = do { simple' <- zonkSimples simple
1824 ; implic' <- mapBagM zonkImplication implic
1825 ; return (WC { wc_simple = simple', wc_impl = implic' }) }
1826
1827 zonkSimples :: Cts -> TcM Cts
1828 zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
1829 ; traceTc "zonkSimples done:" (ppr cts')
1830 ; return cts' }
1831
1832 zonkCt' :: Ct -> TcM Ct
1833 zonkCt' ct = zonkCt ct
1834
1835 {- Note [zonkCt behaviour]
1836 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1837 zonkCt tries to maintain the canonical form of a Ct. For example,
1838 - a CDictCan should stay a CDictCan;
1839 - a CTyEqCan should stay a CTyEqCan (if the LHS stays as a variable.).
1840 - a CHoleCan should stay a CHoleCan
1841 - a CIrredCan should stay a CIrredCan with its cc_insol flag intact
1842
1843 Why?, for example:
1844 - For CDictCan, the @TcSimplify.expandSuperClasses@ step, which runs after the
1845 simple wanted and plugin loop, looks for @CDictCan@s. If a plugin is in use,
1846 constraints are zonked before being passed to the plugin. This means if we
1847 don't preserve a canonical form, @expandSuperClasses@ fails to expand
1848 superclasses. This is what happened in Trac #11525.
1849
1850 - For CHoleCan, once we forget that it's a hole, we can never recover that info.
1851
1852 - For CIrredCan we want to see if a constraint is insoluble with insolubleWC
1853
1854 NB: we do not expect to see any CFunEqCans, because zonkCt is only
1855 called on unflattened constraints.
1856
1857 NB: Constraints are always re-flattened etc by the canonicaliser in
1858 @TcCanonical@ even if they come in as CDictCan. Only canonical constraints that
1859 are actually in the inert set carry all the guarantees. So it is okay if zonkCt
1860 creates e.g. a CDictCan where the cc_tyars are /not/ function free.
1861 -}
1862
1863 zonkCt :: Ct -> TcM Ct
1864 zonkCt ct@(CHoleCan { cc_ev = ev })
1865 = do { ev' <- zonkCtEvidence ev
1866 ; return $ ct { cc_ev = ev' } }
1867
1868 zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
1869 = do { ev' <- zonkCtEvidence ev
1870 ; args' <- mapM zonkTcType args
1871 ; return $ ct { cc_ev = ev', cc_tyargs = args' } }
1872
1873 zonkCt ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs })
1874 = do { ev' <- zonkCtEvidence ev
1875 ; tv_ty' <- zonkTcTyVar tv
1876 ; case getTyVar_maybe tv_ty' of
1877 Just tv' -> do { rhs' <- zonkTcType rhs
1878 ; return ct { cc_ev = ev'
1879 , cc_tyvar = tv'
1880 , cc_rhs = rhs' } }
1881 Nothing -> return (mkNonCanonical ev') }
1882
1883 zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_insol flag
1884 = do { ev' <- zonkCtEvidence ev
1885 ; return (ct { cc_ev = ev' }) }
1886
1887 zonkCt ct
1888 = ASSERT( not (isCFunEqCan ct) )
1889 -- We do not expect to see any CFunEqCans, because zonkCt is only called on
1890 -- unflattened constraints.
1891 do { fl' <- zonkCtEvidence (ctEvidence ct)
1892 ; return (mkNonCanonical fl') }
1893
1894 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
1895 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
1896 = do { pred' <- zonkTcType pred
1897 ; return (ctev { ctev_pred = pred'}) }
1898 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest })
1899 = do { pred' <- zonkTcType pred
1900 ; let dest' = case dest of
1901 EvVarDest ev -> EvVarDest $ setVarType ev pred'
1902 -- necessary in simplifyInfer
1903 HoleDest h -> HoleDest h
1904 ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
1905 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
1906 = do { pred' <- zonkTcType pred
1907 ; return (ctev { ctev_pred = pred' }) }
1908
1909 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
1910 zonkSkolemInfo (SigSkol cx ty tv_prs) = do { ty' <- zonkTcType ty
1911 ; return (SigSkol cx ty' tv_prs) }
1912 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
1913 ; return (InferSkol ntys') }
1914 where
1915 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
1916 zonkSkolemInfo skol_info = return skol_info
1917
1918 {-
1919 %************************************************************************
1920 %* *
1921 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
1922 * *
1923 * For internal use only! *
1924 * *
1925 ************************************************************************
1926
1927 -}
1928
1929 -- zonkId is used *during* typechecking just to zonk the Id's type
1930 zonkId :: TcId -> TcM TcId
1931 zonkId id
1932 = do { ty' <- zonkTcType (idType id)
1933 ; return (Id.setIdType id ty') }
1934
1935 zonkCoVar :: CoVar -> TcM CoVar
1936 zonkCoVar = zonkId
1937
1938 -- | A suitable TyCoMapper for zonking a type during type-checking,
1939 -- before all metavars are filled in.
1940 zonkTcTypeMapper :: TyCoMapper () TcM
1941 zonkTcTypeMapper = TyCoMapper
1942 { tcm_smart = True
1943 , tcm_tyvar = const zonkTcTyVar
1944 , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
1945 , tcm_hole = hole
1946 , tcm_tycobinder = \_env tv _vis -> ((), ) <$> zonkTyCoVarKind tv
1947 , tcm_tycon = zonk_tc_tycon }
1948 where
1949 hole :: () -> CoercionHole -> TcM Coercion
1950 hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
1951 = do { contents <- readTcRef ref
1952 ; case contents of
1953 Just co -> do { co' <- zonkCo co
1954 ; checkCoercionHole cv co' }
1955 Nothing -> do { cv' <- zonkCoVar cv
1956 ; return $ HoleCo (hole { ch_co_var = cv' }) } }
1957
1958 zonk_tc_tycon tc -- A non-poly TcTyCon may have unification
1959 -- variables that need zonking, but poly ones cannot
1960 | tcTyConIsPoly tc = return tc
1961 | otherwise = do { tck' <- zonkTcType (tyConKind tc)
1962 ; return (setTcTyConKind tc tck') }
1963
1964 -- For unbound, mutable tyvars, zonkType uses the function given to it
1965 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
1966 -- type variable and zonks the kind too
1967 zonkTcType :: TcType -> TcM TcType
1968 zonkTcType = mapType zonkTcTypeMapper ()
1969
1970 -- | "Zonk" a coercion -- really, just zonk any types in the coercion
1971 zonkCo :: Coercion -> TcM Coercion
1972 zonkCo = mapCoercion zonkTcTypeMapper ()
1973
1974 zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
1975 -- A tyvar binder is never a unification variable (TauTv),
1976 -- rather it is always a skolem. It *might* be a TyVarTv.
1977 -- (Because non-CUSK type declarations use TyVarTvs.)
1978 -- Regardless, it may have a kind
1979 -- that has not yet been zonked, and may include kind
1980 -- unification variables.
1981 zonkTcTyCoVarBndr tyvar
1982 | isTyVarTyVar tyvar
1983 -- We want to preserve the binding location of the original TyVarTv.
1984 -- This is important for error messages. If we don't do this, then
1985 -- we get bad locations in, e.g., typecheck/should_fail/T2688
1986 = do { zonked_ty <- zonkTcTyVar tyvar
1987 ; let zonked_tyvar = tcGetTyVar "zonkTcTyCoVarBndr TyVarTv" zonked_ty
1988 zonked_name = getName zonked_tyvar
1989 reloc'd_name = setNameLoc zonked_name (getSrcSpan tyvar)
1990 ; return (setTyVarName zonked_tyvar reloc'd_name) }
1991
1992 | otherwise
1993 = ASSERT2( isImmutableTyVar tyvar || isCoVar tyvar, pprTyVar tyvar )
1994 zonkTyCoVarKind tyvar
1995
1996 zonkTyConBinders :: [TyConBinder] -> TcM [TyConBinder]
1997 zonkTyConBinders = mapM zonk1
1998 where
1999 zonk1 (Bndr tv vis)
2000 = do { tv' <- zonkTcTyCoVarBndr tv
2001 ; return (Bndr tv' vis) }
2002
2003 zonkTcTyVar :: TcTyVar -> TcM TcType
2004 -- Simply look through all Flexis
2005 zonkTcTyVar tv
2006 | isTcTyVar tv
2007 = case tcTyVarDetails tv of
2008 SkolemTv {} -> zonk_kind_and_return
2009 RuntimeUnk {} -> zonk_kind_and_return
2010 MetaTv { mtv_ref = ref }
2011 -> do { cts <- readMutVar ref
2012 ; case cts of
2013 Flexi -> zonk_kind_and_return
2014 Indirect ty -> do { zty <- zonkTcType ty
2015 ; writeTcRef ref (Indirect zty)
2016 -- See Note [Sharing in zonking]
2017 ; return zty } }
2018
2019 | otherwise -- coercion variable
2020 = zonk_kind_and_return
2021 where
2022 zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv
2023 ; return (mkTyVarTy z_tv) }
2024
2025 -- Variant that assumes that any result of zonking is still a TyVar.
2026 -- Should be used only on skolems and TyVarTvs
2027 zonkTcTyVarToTyVar :: HasDebugCallStack => TcTyVar -> TcM TcTyVar
2028 zonkTcTyVarToTyVar tv
2029 = do { ty <- zonkTcTyVar tv
2030 ; let tv' = case tcGetTyVar_maybe ty of
2031 Just tv' -> tv'
2032 Nothing -> pprPanic "zonkTcTyVarToTyVar"
2033 (ppr tv $$ ppr ty)
2034 ; return tv' }
2035
2036 zonkTyVarTyVarPairs :: [(Name,TcTyVar)] -> TcM [(Name,TcTyVar)]
2037 zonkTyVarTyVarPairs prs
2038 = mapM do_one prs
2039 where
2040 do_one (nm, tv) = do { tv' <- zonkTcTyVarToTyVar tv
2041 ; return (nm, tv') }
2042
2043 {- Note [Sharing in zonking]
2044 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2045 Suppose we have
2046 alpha :-> beta :-> gamma :-> ty
2047 where the ":->" means that the unification variable has been
2048 filled in with Indirect. Then when zonking alpha, it'd be nice
2049 to short-circuit beta too, so we end up with
2050 alpha :-> zty
2051 beta :-> zty
2052 gamma :-> zty
2053 where zty is the zonked version of ty. That way, if we come across
2054 beta later, we'll have less work to do. (And indeed the same for
2055 alpha.)
2056
2057 This is easily achieved: just overwrite (Indirect ty) with (Indirect
2058 zty). Non-systematic perf comparisons suggest that this is a modest
2059 win.
2060
2061 But c.f Note [Sharing when zonking to Type] in TcHsSyn.
2062
2063 %************************************************************************
2064 %* *
2065 Tidying
2066 * *
2067 ************************************************************************
2068 -}
2069
2070 zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
2071 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
2072 ; return (tidyOpenType env ty') }
2073
2074 zonkTidyTcTypes :: TidyEnv -> [TcType] -> TcM (TidyEnv, [TcType])
2075 zonkTidyTcTypes = zonkTidyTcTypes' []
2076 where zonkTidyTcTypes' zs env [] = return (env, reverse zs)
2077 zonkTidyTcTypes' zs env (ty:tys)
2078 = do { (env', ty') <- zonkTidyTcType env ty
2079 ; zonkTidyTcTypes' (ty':zs) env' tys }
2080
2081 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
2082 zonkTidyOrigin env (GivenOrigin skol_info)
2083 = do { skol_info1 <- zonkSkolemInfo skol_info
2084 ; let skol_info2 = tidySkolemInfo env skol_info1
2085 ; return (env, GivenOrigin skol_info2) }
2086 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act
2087 , uo_expected = exp })
2088 = do { (env1, act') <- zonkTidyTcType env act
2089 ; (env2, exp') <- zonkTidyTcType env1 exp
2090 ; return ( env2, orig { uo_actual = act'
2091 , uo_expected = exp' }) }
2092 zonkTidyOrigin env (KindEqOrigin ty1 m_ty2 orig t_or_k)
2093 = do { (env1, ty1') <- zonkTidyTcType env ty1
2094 ; (env2, m_ty2') <- case m_ty2 of
2095 Just ty2 -> second Just <$> zonkTidyTcType env1 ty2
2096 Nothing -> return (env1, Nothing)
2097 ; (env3, orig') <- zonkTidyOrigin env2 orig
2098 ; return (env3, KindEqOrigin ty1' m_ty2' orig' t_or_k) }
2099 zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
2100 = do { (env1, p1') <- zonkTidyTcType env p1
2101 ; (env2, p2') <- zonkTidyTcType env1 p2
2102 ; return (env2, FunDepOrigin1 p1' l1 p2' l2) }
2103 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
2104 = do { (env1, p1') <- zonkTidyTcType env p1
2105 ; (env2, p2') <- zonkTidyTcType env1 p2
2106 ; (env3, o1') <- zonkTidyOrigin env2 o1
2107 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
2108 zonkTidyOrigin env orig = return (env, orig)
2109
2110 ----------------
2111 tidyCt :: TidyEnv -> Ct -> Ct
2112 -- Used only in error reporting
2113 -- Also converts it to non-canonical
2114 tidyCt env ct
2115 = case ct of
2116 CHoleCan { cc_ev = ev }
2117 -> ct { cc_ev = tidy_ev env ev }
2118 _ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
2119 where
2120 tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
2121 -- NB: we do not tidy the ctev_evar field because we don't
2122 -- show it in error messages
2123 tidy_ev env ctev@(CtGiven { ctev_pred = pred })
2124 = ctev { ctev_pred = tidyType env pred }
2125 tidy_ev env ctev@(CtWanted { ctev_pred = pred })
2126 = ctev { ctev_pred = tidyType env pred }
2127 tidy_ev env ctev@(CtDerived { ctev_pred = pred })
2128 = ctev { ctev_pred = tidyType env pred }
2129
2130 ----------------
2131 tidyEvVar :: TidyEnv -> EvVar -> EvVar
2132 tidyEvVar env var = setVarType var (tidyType env (varType var))
2133
2134 ----------------
2135 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
2136 tidySkolemInfo env (DerivSkol ty) = DerivSkol (tidyType env ty)
2137 tidySkolemInfo env (SigSkol cx ty tv_prs) = tidySigSkol env cx ty tv_prs
2138 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
2139 tidySkolemInfo env (UnifyForAllSkol ty) = UnifyForAllSkol (tidyType env ty)
2140 tidySkolemInfo _ info = info
2141
2142 tidySigSkol :: TidyEnv -> UserTypeCtxt
2143 -> TcType -> [(Name,TcTyVar)] -> SkolemInfo
2144 -- We need to take special care when tidying SigSkol
2145 -- See Note [SigSkol SkolemInfo] in TcRnTypes
2146 tidySigSkol env cx ty tv_prs
2147 = SigSkol cx (tidy_ty env ty) tv_prs'
2148 where
2149 tv_prs' = mapSnd (tidyTyCoVarOcc env) tv_prs
2150 inst_env = mkNameEnv tv_prs'
2151
2152 tidy_ty env (ForAllTy (Bndr tv vis) ty)
2153 = ForAllTy (Bndr tv' vis) (tidy_ty env' ty)
2154 where
2155 (env', tv') = tidy_tv_bndr env tv
2156
2157 tidy_ty env (FunTy arg res)
2158 = FunTy (tidyType env arg) (tidy_ty env res)
2159
2160 tidy_ty env ty = tidyType env ty
2161
2162 tidy_tv_bndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
2163 tidy_tv_bndr env@(occ_env, subst) tv
2164 | Just tv' <- lookupNameEnv inst_env (tyVarName tv)
2165 = ((occ_env, extendVarEnv subst tv tv'), tv')
2166
2167 | otherwise
2168 = tidyVarBndr env tv
2169
2170 -------------------------------------------------------------------------
2171 {-
2172 %************************************************************************
2173 %* *
2174 Levity polymorphism checks
2175 * *
2176 ************************************************************************
2177
2178 See Note [Levity polymorphism checking] in DsMonad
2179
2180 -}
2181
2182 -- | According to the rules around representation polymorphism
2183 -- (see https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds), no binder
2184 -- can have a representation-polymorphic type. This check ensures
2185 -- that we respect this rule. It is a bit regrettable that this error
2186 -- occurs in zonking, after which we should have reported all errors.
2187 -- But it's hard to see where else to do it, because this can be discovered
2188 -- only after all solving is done. And, perhaps most importantly, this
2189 -- isn't really a compositional property of a type system, so it's
2190 -- not a terrible surprise that the check has to go in an awkward spot.
2191 ensureNotLevPoly :: Type -- its zonked type
2192 -> SDoc -- where this happened
2193 -> TcM ()
2194 ensureNotLevPoly ty doc
2195 = whenNoErrs $ -- sometimes we end up zonking bogus definitions of type
2196 -- forall a. a. See, for example, test ghci/scripts/T9140
2197 checkForLevPoly doc ty
2198
2199 -- See Note [Levity polymorphism checking] in DsMonad
2200 checkForLevPoly :: SDoc -> Type -> TcM ()
2201 checkForLevPoly = checkForLevPolyX addErr
2202
2203 checkForLevPolyX :: Monad m
2204 => (SDoc -> m ()) -- how to report an error
2205 -> SDoc -> Type -> m ()
2206 checkForLevPolyX add_err extra ty
2207 | isTypeLevPoly ty
2208 = add_err (formatLevPolyErr ty $$ extra)
2209 | otherwise
2210 = return ()
2211
2212 formatLevPolyErr :: Type -- levity-polymorphic type
2213 -> SDoc
2214 formatLevPolyErr ty
2215 = hang (text "A levity-polymorphic type is not allowed here:")
2216 2 (vcat [ text "Type:" <+> pprWithTYPE tidy_ty
2217 , text "Kind:" <+> pprWithTYPE tidy_ki ])
2218 where
2219 (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty
2220 tidy_ki = tidyType tidy_env (tcTypeKind ty)