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