Rename SigTv to TyVarTv (#15480)
[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,
28 newMetaDetails, 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, cloneWanted, cloneWC,
43 emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
44 newTcEvBinds, newNoTcEvBinds, addTcEvBind,
45
46 newCoercionHole, fillCoercionHole, isFilledCoercionHole,
47 unpackCoercionHole, unpackCoercionHole_maybe,
48 checkCoercionHole,
49
50 --------------------------------
51 -- Instantiation
52 newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
53 newMetaTyVarTyVars, newMetaTyVarTyVarX,
54 newTyVarTyVar, newTauTyVar, newSkolemTyVar, newWildCardX,
55 tcInstType,
56 tcInstSkolTyVars,tcInstSkolTyVarsX,
57 tcInstSuperSkolTyVarsX,
58 tcSkolDFunType, tcSuperSkolTyVars,
59
60 instSkolTyCoVarsX, freshenTyVarBndrs, freshenCoVarBndrsX,
61
62 --------------------------------
63 -- Zonking and tidying
64 zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin,
65 tidyEvVar, tidyCt, tidySkolemInfo,
66 skolemiseRuntimeUnk,
67 zonkTcTyVar, zonkTcTyVars,
68 zonkTcTyVarToTyVar, zonkTyVarTyVarPairs,
69 zonkTyCoVarsAndFV, zonkTcTypeAndFV,
70 zonkTyCoVarsAndFVList,
71 zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
72 zonkQuantifiedTyVar, defaultTyVar,
73 quantifyTyVars,
74 zonkTcTyCoVarBndr, zonkTcTyVarBinder,
75 zonkTcType, zonkTcTypes, zonkCo,
76 zonkTyCoVarKind, zonkTcTypeMapper,
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 Coercion
98 import Class
99 import Var
100
101 -- others:
102 import TcRnMonad -- TcType, amongst others
103 import TcEvidence
104 import Id
105 import Name
106 import VarSet
107 import TysWiredIn
108 import TysPrim
109 import VarEnv
110 import NameEnv
111 import PrelNames
112 import Util
113 import Outputable
114 import FastString
115 import SrcLoc
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
126 {-
127 ************************************************************************
128 * *
129 Kind variables
130 * *
131 ************************************************************************
132 -}
133
134 mkKindName :: Unique -> Name
135 mkKindName unique = mkSystemName unique kind_var_occ
136
137 kind_var_occ :: OccName -- Just one for all MetaKindVars
138 -- They may be jiggled by tidying
139 kind_var_occ = mkOccName tvName "k"
140
141 newMetaKindVar :: TcM TcKind
142 newMetaKindVar = do { uniq <- newUnique
143 ; details <- newMetaDetails TauTv
144 ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
145 ; traceTc "newMetaKindVar" (ppr kv)
146 ; return (mkTyVarTy kv) }
147
148 newMetaKindVars :: Int -> TcM [TcKind]
149 newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
150
151 {-
152 ************************************************************************
153 * *
154 Evidence variables; range over constraints we can abstract over
155 * *
156 ************************************************************************
157 -}
158
159 newEvVars :: TcThetaType -> TcM [EvVar]
160 newEvVars theta = mapM newEvVar theta
161
162 --------------
163
164 newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar
165 -- Creates new *rigid* variables for predicates
166 newEvVar ty = do { name <- newSysName (predTypeOccName ty)
167 ; return (mkLocalIdOrCoVar name ty) }
168
169 newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
170 -- Deals with both equality and non-equality predicates
171 newWanted orig t_or_k pty
172 = do loc <- getCtLocM orig t_or_k
173 d <- if isEqPred pty then HoleDest <$> newCoercionHole pty
174 else EvVarDest <$> newEvVar pty
175 return $ CtWanted { ctev_dest = d
176 , ctev_pred = pty
177 , ctev_nosh = WDeriv
178 , ctev_loc = loc }
179
180 newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
181 newWanteds orig = mapM (newWanted orig Nothing)
182
183 ----------------------------------------------
184 -- Cloning constraints
185 ----------------------------------------------
186
187 cloneWanted :: Ct -> TcM Ct
188 cloneWanted ct
189 | ev@(CtWanted { ctev_dest = HoleDest {}, ctev_pred = pty }) <- ctEvidence ct
190 = do { co_hole <- newCoercionHole pty
191 ; return (mkNonCanonical (ev { ctev_dest = HoleDest co_hole })) }
192 | otherwise
193 = return ct
194
195 cloneWC :: WantedConstraints -> TcM WantedConstraints
196 -- Clone all the evidence bindings in
197 -- a) the ic_bind field of any implications
198 -- b) the CoercionHoles of any wanted constraints
199 -- so that solving the WantedConstraints will not have any visible side
200 -- effect, /except/ from causing unifications
201 cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
202 = do { simples' <- mapBagM cloneWanted simples
203 ; implics' <- mapBagM cloneImplication implics
204 ; return (wc { wc_simple = simples', wc_impl = implics' }) }
205
206 cloneImplication :: Implication -> TcM Implication
207 cloneImplication implic@(Implic { ic_binds = binds, ic_wanted = inner_wanted })
208 = do { binds' <- cloneEvBindsVar binds
209 ; inner_wanted' <- cloneWC inner_wanted
210 ; return (implic { ic_binds = binds', ic_wanted = inner_wanted' }) }
211
212 ----------------------------------------------
213 -- Emitting constraints
214 ----------------------------------------------
215
216 -- | Emits a new Wanted. Deals with both equalities and non-equalities.
217 emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
218 emitWanted origin pty
219 = do { ev <- newWanted origin Nothing pty
220 ; emitSimple $ mkNonCanonical ev
221 ; return $ ctEvTerm ev }
222
223 -- | Emits a new equality constraint
224 emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
225 emitWantedEq origin t_or_k role ty1 ty2
226 = do { hole <- newCoercionHole pty
227 ; loc <- getCtLocM origin (Just t_or_k)
228 ; emitSimple $ mkNonCanonical $
229 CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
230 , ctev_nosh = WDeriv, ctev_loc = loc }
231 ; return (HoleCo hole) }
232 where
233 pty = mkPrimEqPredRole role ty1 ty2
234
235 -- | Creates a new EvVar and immediately emits it as a Wanted.
236 -- No equality predicates here.
237 emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
238 emitWantedEvVar origin ty
239 = do { new_cv <- newEvVar ty
240 ; loc <- getCtLocM origin Nothing
241 ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
242 , ctev_pred = ty
243 , ctev_nosh = WDeriv
244 , ctev_loc = loc }
245 ; emitSimple $ mkNonCanonical ctev
246 ; return new_cv }
247
248 emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
249 emitWantedEvVars orig = mapM (emitWantedEvVar orig)
250
251 newDict :: Class -> [TcType] -> TcM DictId
252 newDict cls tys
253 = do { name <- newSysName (mkDictOcc (getOccName cls))
254 ; return (mkLocalId name (mkClassPred cls tys)) }
255
256 predTypeOccName :: PredType -> OccName
257 predTypeOccName ty = case classifyPredType ty of
258 ClassPred cls _ -> mkDictOcc (getOccName cls)
259 EqPred {} -> mkVarOccFS (fsLit "co")
260 IrredPred {} -> mkVarOccFS (fsLit "irred")
261 ForAllPred {} -> mkVarOccFS (fsLit "df")
262
263 {-
264 ************************************************************************
265 * *
266 Coercion holes
267 * *
268 ************************************************************************
269 -}
270
271 newCoercionHole :: TcPredType -> TcM CoercionHole
272 newCoercionHole pred_ty
273 = do { co_var <- newEvVar pred_ty
274 ; traceTc "New coercion hole:" (ppr co_var)
275 ; ref <- newMutVar Nothing
276 ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } }
277
278 -- | Put a value in a coercion hole
279 fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
280 fillCoercionHole (CoercionHole { ch_ref = ref, ch_co_var = cv }) co
281 = do {
282 #if defined(DEBUG)
283 ; cts <- readTcRef ref
284 ; whenIsJust cts $ \old_co ->
285 pprPanic "Filling a filled coercion hole" (ppr cv $$ ppr co $$ ppr old_co)
286 #endif
287 ; traceTc "Filling coercion hole" (ppr cv <+> text ":=" <+> ppr co)
288 ; writeTcRef ref (Just co) }
289
290 -- | Is a coercion hole filled in?
291 isFilledCoercionHole :: CoercionHole -> TcM Bool
292 isFilledCoercionHole (CoercionHole { ch_ref = ref }) = isJust <$> readTcRef ref
293
294 -- | Retrieve the contents of a coercion hole. Panics if the hole
295 -- is unfilled
296 unpackCoercionHole :: CoercionHole -> TcM Coercion
297 unpackCoercionHole hole
298 = do { contents <- unpackCoercionHole_maybe hole
299 ; case contents of
300 Just co -> return co
301 Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) }
302
303 -- | Retrieve the contents of a coercion hole, if it is filled
304 unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
305 unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref
306
307 -- | Check that a coercion is appropriate for filling a hole. (The hole
308 -- itself is needed only for printing.
309 -- Always returns the checked coercion, but this return value is necessary
310 -- so that the input coercion is forced only when the output is forced.
311 checkCoercionHole :: CoVar -> Coercion -> TcM Coercion
312 checkCoercionHole cv co
313 | debugIsOn
314 = do { cv_ty <- zonkTcType (varType cv)
315 -- co is already zonked, but cv might not be
316 ; return $
317 ASSERT2( ok cv_ty
318 , (text "Bad coercion hole" <+>
319 ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role
320 , ppr cv_ty ]) )
321 co }
322 | otherwise
323 = return co
324
325 where
326 (Pair t1 t2, role) = coercionKindRole co
327 ok cv_ty | EqPred cv_rel cv_t1 cv_t2 <- classifyPredType cv_ty
328 = t1 `eqType` cv_t1
329 && t2 `eqType` cv_t2
330 && role == eqRelRole cv_rel
331 | otherwise
332 = False
333
334 {-
335 ************************************************************************
336 *
337 Expected types
338 *
339 ************************************************************************
340
341 Note [ExpType]
342 ~~~~~~~~~~~~~~
343
344 An ExpType is used as the "expected type" when type-checking an expression.
345 An ExpType can hold a "hole" that can be filled in by the type-checker.
346 This allows us to have one tcExpr that works in both checking mode and
347 synthesis mode (that is, bidirectional type-checking). Previously, this
348 was achieved by using ordinary unification variables, but we don't need
349 or want that generality. (For example, #11397 was caused by doing the
350 wrong thing with unification variables.) Instead, we observe that these
351 holes should
352
353 1. never be nested
354 2. never appear as the type of a variable
355 3. be used linearly (never be duplicated)
356
357 By defining ExpType, separately from Type, we can achieve goals 1 and 2
358 statically.
359
360 See also [wiki:Typechecking]
361
362 Note [TcLevel of ExpType]
363 ~~~~~~~~~~~~~~~~~~~~~~~~~
364 Consider
365
366 data G a where
367 MkG :: G Bool
368
369 foo MkG = True
370
371 This is a classic untouchable-variable / ambiguous GADT return type
372 scenario. But, with ExpTypes, we'll be inferring the type of the RHS.
373 And, because there is only one branch of the case, we won't trigger
374 Note [Case branches must never infer a non-tau type] of TcMatches.
375 We thus must track a TcLevel in an Inferring ExpType. If we try to
376 fill the ExpType and find that the TcLevels don't work out, we
377 fill the ExpType with a tau-tv at the low TcLevel, hopefully to
378 be worked out later by some means. This is triggered in
379 test gadt/gadt-escape1.
380
381 -}
382
383 -- actual data definition is in TcType
384
385 -- | Make an 'ExpType' suitable for inferring a type of kind * or #.
386 newInferExpTypeNoInst :: TcM ExpSigmaType
387 newInferExpTypeNoInst = newInferExpType False
388
389 newInferExpTypeInst :: TcM ExpRhoType
390 newInferExpTypeInst = newInferExpType True
391
392 newInferExpType :: Bool -> TcM ExpType
393 newInferExpType inst
394 = do { u <- newUnique
395 ; tclvl <- getTcLevel
396 ; traceTc "newOpenInferExpType" (ppr u <+> ppr inst <+> ppr tclvl)
397 ; ref <- newMutVar Nothing
398 ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl
399 , ir_ref = ref, ir_inst = inst })) }
400
401 -- | Extract a type out of an ExpType, if one exists. But one should always
402 -- exist. Unless you're quite sure you know what you're doing.
403 readExpType_maybe :: ExpType -> TcM (Maybe TcType)
404 readExpType_maybe (Check ty) = return (Just ty)
405 readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
406
407 -- | Extract a type out of an ExpType. Otherwise, panics.
408 readExpType :: ExpType -> TcM TcType
409 readExpType exp_ty
410 = do { mb_ty <- readExpType_maybe exp_ty
411 ; case mb_ty of
412 Just ty -> return ty
413 Nothing -> pprPanic "Unknown expected type" (ppr exp_ty) }
414
415 -- | Returns the expected type when in checking mode.
416 checkingExpType_maybe :: ExpType -> Maybe TcType
417 checkingExpType_maybe (Check ty) = Just ty
418 checkingExpType_maybe _ = Nothing
419
420 -- | Returns the expected type when in checking mode. Panics if in inference
421 -- mode.
422 checkingExpType :: String -> ExpType -> TcType
423 checkingExpType _ (Check ty) = ty
424 checkingExpType err et = pprPanic "checkingExpType" (text err $$ ppr et)
425
426 tauifyExpType :: ExpType -> TcM ExpType
427 -- ^ Turn a (Infer hole) type into a (Check alpha),
428 -- where alpha is a fresh unification variable
429 tauifyExpType (Check ty) = return (Check ty) -- No-op for (Check ty)
430 tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res
431 ; return (Check ty) }
432
433 -- | Extracts the expected type if there is one, or generates a new
434 -- TauTv if there isn't.
435 expTypeToType :: ExpType -> TcM TcType
436 expTypeToType (Check ty) = return ty
437 expTypeToType (Infer inf_res) = inferResultToType inf_res
438
439 inferResultToType :: InferResult -> TcM Type
440 inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
441 , ir_ref = ref })
442 = do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
443 ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
444 -- See Note [TcLevel of ExpType]
445 ; writeMutVar ref (Just tau)
446 ; traceTc "Forcing ExpType to be monomorphic:"
447 (ppr u <+> text ":=" <+> ppr tau)
448 ; return tau }
449
450
451 {- *********************************************************************
452 * *
453 SkolemTvs (immutable)
454 * *
455 ********************************************************************* -}
456
457 tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
458 -- ^ How to instantiate the type variables
459 -> Id -- ^ Type to instantiate
460 -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result
461 -- (type vars, preds (incl equalities), rho)
462 tcInstType inst_tyvars id
463 = case tcSplitForAllTys (idType id) of
464 ([], rho) -> let -- There may be overloading despite no type variables;
465 -- (?x :: Int) => Int -> Int
466 (theta, tau) = tcSplitPhiTy rho
467 in
468 return ([], theta, tau)
469
470 (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
471 ; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho)
472 tv_prs = map tyVarName tyvars `zip` tyvars'
473 ; return (tv_prs, theta, tau) }
474
475 tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
476 -- Instantiate a type signature with skolem constants.
477 -- We could give them fresh names, but no need to do so
478 tcSkolDFunType dfun
479 = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
480 ; return (map snd tv_prs, theta, tau) }
481
482 tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
483 -- Make skolem constants, but do *not* give them new names, as above
484 -- Moreover, make them "super skolems"; see comments with superSkolemTv
485 -- see Note [Kind substitution when instantiating]
486 -- Precondition: tyvars should be ordered by scoping
487 tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
488
489 tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
490 tcSuperSkolTyVar subst tv
491 = (extendTvSubstWithClone subst tv new_tv, new_tv)
492 where
493 kind = substTyUnchecked subst (tyVarKind tv)
494 new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
495
496 -- | Given a list of @['TyVar']@, skolemize the type variables,
497 -- returning a substitution mapping the original tyvars to the
498 -- skolems, and the list of newly bound skolems. See also
499 -- tcInstSkolTyVars' for a precondition. The resulting
500 -- skolems are non-overlappable; see Note [Overlap and deriving]
501 -- for an example where this matters.
502 tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
503 tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst
504
505 tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
506 tcInstSkolTyVarsX = tcInstSkolTyVars' False
507
508 tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
509 tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
510
511 tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
512 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
513
514 tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
515 -- Precondition: tyvars should be ordered (kind vars first)
516 -- see Note [Kind substitution when instantiating]
517 -- Get the location from the monad; this is a complete freshening operation
518 tcInstSkolTyVars' overlappable subst tvs
519 = do { loc <- getSrcSpanM
520 ; lvl <- getTcLevel
521 ; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs }
522
523 mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyCoVarMaker gbl lcl
524 -- Allocates skolems whose level is ONE GREATER THAN the passed-in tc_lvl
525 -- See Note [Skolem level allocation]
526 mkTcSkolTyVar tc_lvl loc overlappable old_name kind
527 = do { uniq <- newUnique
528 ; let name = mkInternalName uniq (getOccName old_name) loc
529 ; return (mkTcTyVar name kind details) }
530 where
531 details = SkolemTv (pushTcLevel tc_lvl) overlappable
532 -- pushTcLevel: see Note [Skolem level allocation]
533
534 {- Note [Skolem level allocation]
535 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
536 We generally allocate skolems /before/ calling pushLevelAndCaptureConstraints.
537 So we want their level to the level of the soon-to-be-created implication,
538 which has a level one higher than the current level. Hence the pushTcLevel.
539 It feels like a slight hack. Applies also to vanillaSkolemTv.
540
541 -}
542
543 ------------------
544 freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
545 -- ^ Give fresh uniques to a bunch of TyVars, but they stay
546 -- as TyVars, rather than becoming TcTyVars
547 -- Used in FamInst.newFamInst, and Inst.newClsInst
548 freshenTyVarBndrs = instSkolTyCoVars mk_tv
549 where
550 mk_tv old_name kind
551 = do { uniq <- newUnique
552 ; return (mkTyVar (setNameUnique old_name uniq) kind) }
553
554 freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcRnIf gbl lcl (TCvSubst, [CoVar])
555 -- ^ Give fresh uniques to a bunch of CoVars
556 -- Used in FamInst.newFamInst
557 freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
558 where
559 mk_cv old_name kind
560 = do { uniq <- newUnique
561 ; return (mkCoVar (setNameUnique old_name uniq) kind) }
562
563 ------------------
564 type TcTyCoVarMaker gbl lcl = Name -> Kind -> TcRnIf gbl lcl TyCoVar
565 -- The TcTyCoVarMaker should make a fresh Name, based on the old one
566 -- Freshness is critical. See Note [Skolems in zonkSyntaxExpr] in TcHsSyn
567
568 instSkolTyCoVars :: TcTyCoVarMaker gbl lcl -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
569 instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
570
571 instSkolTyCoVarsX :: TcTyCoVarMaker gbl lcl
572 -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
573 instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
574
575 instSkolTyCoVarX :: TcTyCoVarMaker gbl lcl
576 -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
577 instSkolTyCoVarX mk_tcv subst tycovar
578 = do { new_tcv <- mk_tcv old_name kind
579 ; let subst1 | isTyVar new_tcv
580 = extendTvSubstWithClone subst tycovar new_tcv
581 | otherwise
582 = extendCvSubstWithClone subst tycovar new_tcv
583 ; return (subst1, new_tcv) }
584 where
585 old_name = tyVarName tycovar
586 kind = substTyUnchecked subst (tyVarKind tycovar)
587
588 newFskTyVar :: TcType -> TcM TcTyVar
589 newFskTyVar fam_ty
590 = do { uniq <- newUnique
591 ; ref <- newMutVar Flexi
592 ; tclvl <- getTcLevel
593 ; let details = MetaTv { mtv_info = FlatSkolTv
594 , mtv_ref = ref
595 , mtv_tclvl = tclvl }
596 name = mkMetaTyVarName uniq (fsLit "fsk")
597 ; return (mkTcTyVar name (typeKind fam_ty) details) }
598
599 {-
600 Note [Kind substitution when instantiating]
601 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
602 When we instantiate a bunch of kind and type variables, first we
603 expect them to be topologically sorted.
604 Then we have to instantiate the kind variables, build a substitution
605 from old variables to the new variables, then instantiate the type
606 variables substituting the original kind.
607
608 Exemple: If we want to instantiate
609 [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
610 we want
611 [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
612 instead of the buggous
613 [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
614
615
616 ************************************************************************
617 * *
618 MetaTvs (meta type variables; mutable)
619 * *
620 ************************************************************************
621 -}
622
623 {-
624 Note [TyVarTv]
625 ~~~~~~~~~~~~
626
627 A TyVarTv can unify with type *variables* only, including other TyVarTvs and
628 skolems. Sometimes, they can unify with type variables that the user would
629 rather keep distinct; see #11203 for an example. So, any client of this
630 function needs to either allow the TyVarTvs to unify with each other or check
631 that they don't (say, with a call to findDubTyVarTvs).
632
633 Before #15050 this (under the name SigTv) was used for ScopedTypeVariables in
634 patterns, to make sure these type variables only refer to other type variables,
635 but this restriction was dropped, and ScopedTypeVariables can now refer to full
636 types (GHC Proposal 29).
637
638 The remaining uses of newTyVarTyVars are
639 * in kind signatures, see Note [Kind generalisation and TyVarTvs]
640 and Note [Use TyVarTvs in kind-checking pass]
641 * in partial type signatures, see Note [Quantified variables in partial type signatures]
642 -}
643
644 -- see Note [TyVarTv]
645 newTyVarTyVar :: Name -> Kind -> TcM TcTyVar
646 newTyVarTyVar name kind
647 = do { details <- newMetaDetails TyVarTv
648 ; let tyvar = mkTcTyVar name kind details
649 ; traceTc "newTyVarTyVar" (ppr tyvar)
650 ; return tyvar }
651
652
653 -- makes a new skolem tv
654 newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
655 newSkolemTyVar name kind = do { lvl <- getTcLevel
656 ; return (mkTcTyVar name kind (SkolemTv lvl False)) }
657
658 newFmvTyVar :: TcType -> TcM TcTyVar
659 -- Very like newMetaTyVar, except sets mtv_tclvl to one less
660 -- so that the fmv is untouchable.
661 newFmvTyVar fam_ty
662 = do { uniq <- newUnique
663 ; ref <- newMutVar Flexi
664 ; tclvl <- getTcLevel
665 ; let details = MetaTv { mtv_info = FlatMetaTv
666 , mtv_ref = ref
667 , mtv_tclvl = tclvl }
668 name = mkMetaTyVarName uniq (fsLit "s")
669 ; return (mkTcTyVar name (typeKind fam_ty) details) }
670
671 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
672 newMetaDetails info
673 = do { ref <- newMutVar Flexi
674 ; tclvl <- getTcLevel
675 ; return (MetaTv { mtv_info = info
676 , mtv_ref = ref
677 , mtv_tclvl = tclvl }) }
678
679 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
680 cloneMetaTyVar tv
681 = ASSERT( isTcTyVar tv )
682 do { uniq <- newUnique
683 ; ref <- newMutVar Flexi
684 ; let name' = setNameUnique (tyVarName tv) uniq
685 details' = case tcTyVarDetails tv of
686 details@(MetaTv {}) -> details { mtv_ref = ref }
687 _ -> pprPanic "cloneMetaTyVar" (ppr tv)
688 tyvar = mkTcTyVar name' (tyVarKind tv) details'
689 ; traceTc "cloneMetaTyVar" (ppr tyvar)
690 ; return tyvar }
691
692 -- Works for both type and kind variables
693 readMetaTyVar :: TyVar -> TcM MetaDetails
694 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
695 readMutVar (metaTyVarRef tyvar)
696
697 isFilledMetaTyVar :: TyVar -> TcM Bool
698 -- True of a filled-in (Indirect) meta type variable
699 isFilledMetaTyVar tv
700 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
701 = do { details <- readMutVar ref
702 ; return (isIndirect details) }
703 | otherwise = return False
704
705 isUnfilledMetaTyVar :: TyVar -> TcM Bool
706 -- True of a un-filled-in (Flexi) meta type variable
707 isUnfilledMetaTyVar tv
708 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
709 = do { details <- readMutVar ref
710 ; return (isFlexi details) }
711 | otherwise = return False
712
713 --------------------
714 -- Works with both type and kind variables
715 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
716 -- Write into a currently-empty MetaTyVar
717
718 writeMetaTyVar tyvar ty
719 | not debugIsOn
720 = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty
721
722 -- Everything from here on only happens if DEBUG is on
723 | not (isTcTyVar tyvar)
724 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
725 return ()
726
727 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
728 = writeMetaTyVarRef tyvar ref ty
729
730 | otherwise
731 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
732 return ()
733
734 --------------------
735 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
736 -- Here the tyvar is for error checking only;
737 -- the ref cell must be for the same tyvar
738 writeMetaTyVarRef tyvar ref ty
739 | not debugIsOn
740 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
741 <+> text ":=" <+> ppr ty)
742 ; writeTcRef ref (Indirect ty) }
743
744 -- Everything from here on only happens if DEBUG is on
745 | otherwise
746 = do { meta_details <- readMutVar ref;
747 -- Zonk kinds to allow the error check to work
748 ; zonked_tv_kind <- zonkTcType tv_kind
749 ; zonked_ty <- zonkTcType ty
750 ; let zonked_ty_kind = typeKind zonked_ty -- need to zonk even before typeKind;
751 -- otherwise, we can panic in piResultTy
752 kind_check_ok = tcIsConstraintKind zonked_tv_kind
753 || tcEqKind zonked_ty_kind zonked_tv_kind
754 -- Hack alert! tcIsConstraintKind: see TcHsType
755 -- Note [Extra-constraint holes in partial type signatures]
756
757 kind_msg = hang (text "Ill-kinded update to meta tyvar")
758 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
759 <+> text ":="
760 <+> ppr ty <+> text "::" <+> (ppr zonked_ty_kind) )
761
762 ; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
763
764 -- Check for double updates
765 ; MASSERT2( isFlexi meta_details, double_upd_msg meta_details )
766
767 -- Check for level OK
768 -- See Note [Level check when unifying]
769 ; MASSERT2( level_check_ok, level_check_msg )
770
771 -- Check Kinds ok
772 ; MASSERT2( kind_check_ok, kind_msg )
773
774 -- Do the write
775 ; writeMutVar ref (Indirect ty) }
776 where
777 tv_kind = tyVarKind tyvar
778
779 tv_lvl = tcTyVarLevel tyvar
780 ty_lvl = tcTypeLevel ty
781
782 level_check_ok = not (ty_lvl `strictlyDeeperThan` tv_lvl)
783 level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
784
785 double_upd_msg details = hang (text "Double update of meta tyvar")
786 2 (ppr tyvar $$ ppr details)
787
788
789 {- Note [Level check when unifying]
790 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
791 When unifying
792 alpha:lvl := ty
793 we expect that the TcLevel of 'ty' will be <= lvl.
794 However, during unflatting we do
795 fuv:l := ty:(l+1)
796 which is usually wrong; hence the check isFmmvTyVar in level_check_ok.
797 See Note [TcLevel assignment] in TcType.
798 -}
799
800 {-
801 % Generating fresh variables for pattern match check
802 -}
803
804
805 {-
806 ************************************************************************
807 * *
808 MetaTvs: TauTvs
809 * *
810 ************************************************************************
811
812 Note [Never need to instantiate coercion variables]
813 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
814 With coercion variables sloshing around in types, it might seem that we
815 sometimes need to instantiate coercion variables. This would be problematic,
816 because coercion variables inhabit unboxed equality (~#), and the constraint
817 solver thinks in terms only of boxed equality (~). The solution is that
818 we never need to instantiate coercion variables in the first place.
819
820 The tyvars that we need to instantiate come from the types of functions,
821 data constructors, and patterns. These will never be quantified over
822 coercion variables, except for the special case of the promoted Eq#. But,
823 that can't ever appear in user code, so we're safe!
824 -}
825
826 newTauTyVar :: Name -> Kind -> TcM TcTyVar
827 newTauTyVar name kind
828 = do { details <- newMetaDetails TauTv
829 ; let tyvar = mkTcTyVar name kind details
830 ; traceTc "newTauTyVar" (ppr tyvar)
831 ; return tyvar }
832
833
834 mkMetaTyVarName :: Unique -> FastString -> Name
835 -- Makes a /System/ Name, which is eagerly eliminated by
836 -- the unifier; see TcUnify.nicer_to_update_tv1, and
837 -- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
838 mkMetaTyVarName uniq str = mkSystemName uniq (mkTyVarOccFS str)
839
840 newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
841 -- Make a new meta tyvar out of thin air
842 newAnonMetaTyVar meta_info kind
843 = do { uniq <- newUnique
844 ; let name = mkMetaTyVarName uniq s
845 s = case meta_info of
846 TauTv -> fsLit "t"
847 FlatMetaTv -> fsLit "fmv"
848 FlatSkolTv -> fsLit "fsk"
849 TyVarTv -> fsLit "a"
850 ; details <- newMetaDetails meta_info
851 ; let tyvar = mkTcTyVar name kind details
852 ; traceTc "newAnonMetaTyVar" (ppr tyvar)
853 ; return tyvar }
854
855 cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
856 -- Same as newAnonMetaTyVar, but use a supplied TyVar as the source of the print-name
857 cloneAnonMetaTyVar info tv kind
858 = do { uniq <- newUnique
859 ; details <- newMetaDetails info
860 ; let name = mkSystemName uniq (getOccName tv)
861 -- See Note [Name of an instantiated type variable]
862 tyvar = mkTcTyVar name kind details
863 ; traceTc "cloneAnonMetaTyVar" (ppr tyvar)
864 ; return tyvar }
865
866 {- Note [Name of an instantiated type variable]
867 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
868 At the moment we give a unification variable a System Name, which
869 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
870 -}
871
872 newFlexiTyVar :: Kind -> TcM TcTyVar
873 newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
874
875 newFlexiTyVarTy :: Kind -> TcM TcType
876 newFlexiTyVarTy kind = do
877 tc_tyvar <- newFlexiTyVar kind
878 return (mkTyVarTy tc_tyvar)
879
880 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
881 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
882
883 newOpenTypeKind :: TcM TcKind
884 newOpenTypeKind
885 = do { rr <- newFlexiTyVarTy runtimeRepTy
886 ; return (tYPE rr) }
887
888 -- | Create a tyvar that can be a lifted or unlifted type.
889 -- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh
890 newOpenFlexiTyVarTy :: TcM TcType
891 newOpenFlexiTyVarTy
892 = do { kind <- newOpenTypeKind
893 ; newFlexiTyVarTy kind }
894
895 newMetaTyVarTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
896 newMetaTyVarTyVars = mapAccumLM newMetaTyVarTyVarX emptyTCvSubst
897
898 newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
899 -- Instantiate with META type variables
900 -- Note that this works for a sequence of kind, type, and coercion variables
901 -- variables. Eg [ (k:*), (a:k->k) ]
902 -- Gives [ (k7:*), (a8:k7->k7) ]
903 newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
904 -- emptyTCvSubst has an empty in-scope set, but that's fine here
905 -- Since the tyvars are freshly made, they cannot possibly be
906 -- captured by any existing for-alls.
907
908 newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
909 -- Make a new unification variable tyvar whose Name and Kind come from
910 -- an existing TyVar. We substitute kind variables in the kind.
911 newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
912
913 newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
914 -- Just like newMetaTyVars, but start with an existing substitution.
915 newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
916
917 newMetaTyVarTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
918 -- Just like newMetaTyVarX, but make a TyVarTv
919 newMetaTyVarTyVarX subst tyvar = new_meta_tv_x TyVarTv subst tyvar
920
921 newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
922 newWildCardX subst tv
923 = do { new_tv <- newAnonMetaTyVar TauTv (substTy subst (tyVarKind tv))
924 ; return (extendTvSubstWithClone subst tv new_tv, new_tv) }
925
926 new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
927 new_meta_tv_x info subst tv
928 = do { new_tv <- cloneAnonMetaTyVar info tv substd_kind
929 ; let subst1 = extendTvSubstWithClone subst tv new_tv
930 ; return (subst1, new_tv) }
931 where
932 substd_kind = substTyUnchecked subst (tyVarKind tv)
933 -- NOTE: Trac #12549 is fixed so we could use
934 -- substTy here, but the tc_infer_args problem
935 -- is not yet fixed so leaving as unchecked for now.
936 -- OLD NOTE:
937 -- Unchecked because we call newMetaTyVarX from
938 -- tcInstTyBinder, which is called from tcInferApps
939 -- which does not yet take enough trouble to ensure
940 -- the in-scope set is right; e.g. Trac #12785 trips
941 -- if we use substTy here
942
943 newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
944 newMetaTyVarTyAtLevel tc_lvl kind
945 = do { uniq <- newUnique
946 ; ref <- newMutVar Flexi
947 ; let name = mkMetaTyVarName uniq (fsLit "p")
948 details = MetaTv { mtv_info = TauTv
949 , mtv_ref = ref
950 , mtv_tclvl = tc_lvl }
951 ; return (mkTyVarTy (mkTcTyVar name kind details)) }
952
953 {- *********************************************************************
954 * *
955 Quantification
956 * *
957 ************************************************************************
958
959 Note [quantifyTyVars]
960 ~~~~~~~~~~~~~~~~~~~~~
961 quantifyTyVars is given the free vars of a type that we
962 are about to wrap in a forall.
963
964 It takes these free type/kind variables (partitioned into dependent and
965 non-dependent variables) and
966 1. Zonks them and remove globals and covars
967 2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
968 3. Calls zonkQuantifiedTyVar on each
969
970 Step (2) is often unimportant, because the kind variable is often
971 also free in the type. Eg
972 Typeable k (a::k)
973 has free vars {k,a}. But the type (see Trac #7916)
974 (f::k->*) (a::k)
975 has free vars {f,a}, but we must add 'k' as well! Hence step (2).
976
977 * This function distinguishes between dependent and non-dependent
978 variables only to keep correct defaulting behavior with -XNoPolyKinds.
979 With -XPolyKinds, it treats both classes of variables identically.
980
981 * quantifyTyVars never quantifies over
982 - a coercion variable
983 - a runtime-rep variable
984
985 Note [quantifyTyVars determinism]
986 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
987 The results of quantifyTyVars are wrapped in a forall and can end up in the
988 interface file. One such example is inferred type signatures. They also affect
989 the results of optimizations, for example worker-wrapper. This means that to
990 get deterministic builds quantifyTyVars needs to be deterministic.
991
992 To achieve this CandidatesQTvs is backed by deterministic sets which allows them
993 to be later converted to a list in a deterministic order.
994
995 For more information about deterministic sets see
996 Note [Deterministic UniqFM] in UniqDFM.
997 -}
998
999 quantifyTyVars
1000 :: TcTyCoVarSet -- Global tvs; already zonked
1001 -> CandidatesQTvs -- See Note [Dependent type variables] in TcType
1002 -- Already zonked
1003 -> TcM [TcTyVar]
1004 -- See Note [quantifyTyVars]
1005 -- Can be given a mixture of TcTyVars and TyVars, in the case of
1006 -- associated type declarations. Also accepts covars, but *never* returns any.
1007
1008 quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
1009 = do { traceTc "quantifyTyVars" (vcat [ppr dvs, ppr gbl_tvs])
1010 ; let dep_kvs = dVarSetElemsWellScoped $
1011 dep_tkvs `dVarSetMinusVarSet` gbl_tvs
1012 -- dVarSetElemsWellScoped: put the kind variables into
1013 -- well-scoped order.
1014 -- E.g. [k, (a::k)] not the other way roud
1015
1016 nondep_tvs = dVarSetElems $
1017 (nondep_tkvs `minusDVarSet` dep_tkvs)
1018 `dVarSetMinusVarSet` gbl_tvs
1019 -- See Note [Dependent type variables] in TcType
1020 -- The `minus` dep_tkvs removes any kind-level vars
1021 -- e.g. T k (a::k) Since k appear in a kind it'll
1022 -- be in dv_kvs, and is dependent. So remove it from
1023 -- dv_tvs which will also contain k
1024 -- No worry about dependent covars here;
1025 -- they are all in dep_tkvs
1026 -- No worry about scoping, because these are all
1027 -- type variables
1028 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
1029
1030 -- In the non-PolyKinds case, default the kind variables
1031 -- to *, and zonk the tyvars as usual. Notice that this
1032 -- may make quantifyTyVars return a shorter list
1033 -- than it was passed, but that's ok
1034 ; poly_kinds <- xoptM LangExt.PolyKinds
1035 ; dep_kvs' <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs
1036 ; nondep_tvs' <- mapMaybeM (zonk_quant False) nondep_tvs
1037 ; let final_qtvs = dep_kvs' ++ nondep_tvs'
1038 -- Because of the order, any kind variables
1039 -- mentioned in the kinds of the nondep_tvs'
1040 -- now refer to the dep_kvs'
1041
1042 ; traceTc "quantifyTyVars"
1043 (vcat [ text "globals:" <+> ppr gbl_tvs
1044 , text "nondep:" <+> pprTyVars nondep_tvs
1045 , text "dep:" <+> pprTyVars dep_kvs
1046 , text "dep_kvs'" <+> pprTyVars dep_kvs'
1047 , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ])
1048
1049 -- We should never quantify over coercion variables; check this
1050 ; let co_vars = filter isCoVar final_qtvs
1051 ; MASSERT2( null co_vars, ppr co_vars )
1052
1053 ; return final_qtvs }
1054 where
1055 -- zonk_quant returns a tyvar if it should be quantified over;
1056 -- otherwise, it returns Nothing. The latter case happens for
1057 -- * Kind variables, with -XNoPolyKinds: don't quantify over these
1058 -- * RuntimeRep variables: we never quantify over these
1059 zonk_quant default_kind tkv
1060 | not (isTyVar tkv)
1061 = return Nothing -- this can happen for a covar that's associated with
1062 -- a coercion hole. Test case: typecheck/should_compile/T2494
1063
1064 | not (isTcTyVar tkv)
1065 = return (Just tkv) -- For associated types, we have the class variables
1066 -- in scope, and they are TyVars not TcTyVars
1067 | otherwise
1068 = do { deflt_done <- defaultTyVar default_kind tkv
1069 ; case deflt_done of
1070 True -> return Nothing
1071 False -> do { tv <- zonkQuantifiedTyVar tkv
1072 ; return (Just tv) } }
1073
1074 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
1075 -- The quantified type variables often include meta type variables
1076 -- we want to freeze them into ordinary type variables
1077 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
1078 -- bound occurrences of the original type variable will get zonked to
1079 -- the immutable version.
1080 --
1081 -- We leave skolem TyVars alone; they are immutable.
1082 --
1083 -- This function is called on both kind and type variables,
1084 -- but kind variables *only* if PolyKinds is on.
1085
1086 zonkQuantifiedTyVar tv
1087 = case tcTyVarDetails tv of
1088 SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
1089 ; return (setTyVarKind tv kind) }
1090 -- It might be a skolem type variable,
1091 -- for example from a user type signature
1092
1093 MetaTv {} -> skolemiseUnboundMetaTyVar tv
1094
1095 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- RuntimeUnk
1096
1097 defaultTyVar :: Bool -- True <=> please default this kind variable to *
1098 -> TcTyVar -- If it's a MetaTyVar then it is unbound
1099 -> TcM Bool -- True <=> defaulted away altogether
1100
1101 defaultTyVar default_kind tv
1102 | not (isMetaTyVar tv)
1103 = return False
1104
1105 | isTyVarTyVar tv
1106 -- Do not default TyVarTvs. Doing so would violate the invariants
1107 -- on TyVarTvs; see Note [Signature skolems] in TcType.
1108 -- Trac #13343 is an example; #14555 is another
1109 -- See Note [Kind generalisation and TyVarTvs]
1110 = return False
1111
1112
1113 | isRuntimeRepVar tv -- Do not quantify over a RuntimeRep var
1114 -- unless it is a TyVarTv, handled earlier
1115 = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
1116 ; writeMetaTyVar tv liftedRepTy
1117 ; return True }
1118
1119 | default_kind -- -XNoPolyKinds and this is a kind var
1120 = do { default_kind_var tv -- so default it to * if possible
1121 ; return True }
1122
1123 | otherwise
1124 = return False
1125
1126 where
1127 default_kind_var :: TyVar -> TcM ()
1128 -- defaultKindVar is used exclusively with -XNoPolyKinds
1129 -- See Note [Defaulting with -XNoPolyKinds]
1130 -- It takes an (unconstrained) meta tyvar and defaults it.
1131 -- Works only on vars of type *; for other kinds, it issues an error.
1132 default_kind_var kv
1133 | isLiftedTypeKind (tyVarKind kv)
1134 = do { traceTc "Defaulting a kind var to *" (ppr kv)
1135 ; writeMetaTyVar kv liftedTypeKind }
1136 | otherwise
1137 = addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
1138 , text "of kind:" <+> ppr (tyVarKind kv')
1139 , text "Perhaps enable PolyKinds or add a kind signature" ])
1140 where
1141 (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
1142
1143 skolemiseRuntimeUnk :: TcTyVar -> TcM TyVar
1144 skolemiseRuntimeUnk tv
1145 = skolemise_tv tv RuntimeUnk
1146
1147 skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar
1148 skolemiseUnboundMetaTyVar tv
1149 = skolemise_tv tv (SkolemTv (metaTyVarTcLevel tv) False)
1150
1151 skolemise_tv :: TcTyVar -> TcTyVarDetails -> TcM TyVar
1152 -- We have a Meta tyvar with a ref-cell inside it
1153 -- Skolemise it, so that
1154 -- we are totally out of Meta-tyvar-land
1155 -- We create a skolem TyVar, not a regular TyVar
1156 -- See Note [Zonking to Skolem]
1157 skolemise_tv tv details
1158 = ASSERT2( isMetaTyVar tv, ppr tv )
1159 do { when debugIsOn (check_empty tv)
1160 ; span <- getSrcSpanM -- Get the location from "here"
1161 -- ie where we are generalising
1162 ; kind <- zonkTcType (tyVarKind tv)
1163 ; let uniq = getUnique tv
1164 -- NB: Use same Unique as original tyvar. This is
1165 -- important for TcHsType.splitTelescopeTvs to work properly
1166
1167 tv_name = getOccName tv
1168 final_name = mkInternalName uniq tv_name span
1169 final_tv = mkTcTyVar final_name kind details
1170
1171 ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
1172 ; writeMetaTyVar tv (mkTyVarTy final_tv)
1173 ; return final_tv }
1174
1175 where
1176 check_empty tv -- [Sept 04] Check for non-empty.
1177 = when debugIsOn $ -- See note [Silly Type Synonym]
1178 do { cts <- readMetaTyVar tv
1179 ; case cts of
1180 Flexi -> return ()
1181 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
1182 return () }
1183
1184 {- Note [Defaulting with -XNoPolyKinds]
1185 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1186 Consider
1187
1188 data Compose f g a = Mk (f (g a))
1189
1190 We infer
1191
1192 Compose :: forall k1 k2. (k2 -> *) -> (k1 -> k2) -> k1 -> *
1193 Mk :: forall k1 k2 (f :: k2 -> *) (g :: k1 -> k2) (a :: k1).
1194 f (g a) -> Compose k1 k2 f g a
1195
1196 Now, in another module, we have -XNoPolyKinds -XDataKinds in effect.
1197 What does 'Mk mean? Pre GHC-8.0 with -XNoPolyKinds,
1198 we just defaulted all kind variables to *. But that's no good here,
1199 because the kind variables in 'Mk aren't of kind *, so defaulting to *
1200 is ill-kinded.
1201
1202 After some debate on #11334, we decided to issue an error in this case.
1203 The code is in defaultKindVar.
1204
1205 Note [What is a meta variable?]
1206 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1207 A "meta type-variable", also know as a "unification variable" is a placeholder
1208 introduced by the typechecker for an as-yet-unknown monotype.
1209
1210 For example, when we see a call `reverse (f xs)`, we know that we calling
1211 reverse :: forall a. [a] -> [a]
1212 So we know that the argument `f xs` must be a "list of something". But what is
1213 the "something"? We don't know until we explore the `f xs` a bit more. So we set
1214 out what we do know at the call of `reverse` by instantiate its type with a fresh
1215 meta tyvar, `alpha` say. So now the type of the argument `f xs`, and of the
1216 result, is `[alpha]`. The unification variable `alpha` stands for the
1217 as-yet-unknown type of the elements of the list.
1218
1219 As type inference progresses we may learn more about `alpha`. For example, suppose
1220 `f` has the type
1221 f :: forall b. b -> [Maybe b]
1222 Then we instantiate `f`'s type with another fresh unification variable, say
1223 `beta`; and equate `f`'s result type with reverse's argument type, thus
1224 `[alpha] ~ [Maybe beta]`.
1225
1226 Now we can solve this equality to learn that `alpha ~ Maybe beta`, so we've
1227 refined our knowledge about `alpha`. And so on.
1228
1229 If you found this Note useful, you may also want to have a look at
1230 Section 5 of "Practical type inference for higher rank types" (Peyton Jones,
1231 Vytiniotis, Weirich and Shields. J. Functional Programming. 2011).
1232
1233 Note [What is zonking?]
1234 ~~~~~~~~~~~~~~~~~~~~~~~
1235 GHC relies heavily on mutability in the typechecker for efficient operation.
1236 For this reason, throughout much of the type checking process meta type
1237 variables (the MetaTv constructor of TcTyVarDetails) are represented by mutable
1238 variables (known as TcRefs).
1239
1240 Zonking is the process of ripping out these mutable variables and replacing them
1241 with a real Type. This involves traversing the entire type expression, but the
1242 interesting part of replacing the mutable variables occurs in zonkTyVarOcc.
1243
1244 There are two ways to zonk a Type:
1245
1246 * zonkTcTypeToType, which is intended to be used at the end of type-checking
1247 for the final zonk. It has to deal with unfilled metavars, either by filling
1248 it with a value like Any or failing (determined by the UnboundTyVarZonker
1249 used).
1250
1251 * zonkTcType, which will happily ignore unfilled metavars. This is the
1252 appropriate function to use while in the middle of type-checking.
1253
1254 Note [Zonking to Skolem]
1255 ~~~~~~~~~~~~~~~~~~~~~~~~
1256 We used to zonk quantified type variables to regular TyVars. However, this
1257 leads to problems. Consider this program from the regression test suite:
1258
1259 eval :: Int -> String -> String -> String
1260 eval 0 root actual = evalRHS 0 root actual
1261
1262 evalRHS :: Int -> a
1263 evalRHS 0 root actual = eval 0 root actual
1264
1265 It leads to the deferral of an equality (wrapped in an implication constraint)
1266
1267 forall a. () => ((String -> String -> String) ~ a)
1268
1269 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
1270 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
1271 This has the *side effect* of also zonking the `a' in the deferred equality
1272 (which at this point is being handed around wrapped in an implication
1273 constraint).
1274
1275 Finally, the equality (with the zonked `a') will be handed back to the
1276 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
1277 If we zonk `a' with a regular type variable, we will have this regular type
1278 variable now floating around in the simplifier, which in many places assumes to
1279 only see proper TcTyVars.
1280
1281 We can avoid this problem by zonking with a skolem. The skolem is rigid
1282 (which we require for a quantified variable), but is still a TcTyVar that the
1283 simplifier knows how to deal with.
1284
1285 Note [Silly Type Synonyms]
1286 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1287 Consider this:
1288 type C u a = u -- Note 'a' unused
1289
1290 foo :: (forall a. C u a -> C u a) -> u
1291 foo x = ...
1292
1293 bar :: Num u => u
1294 bar = foo (\t -> t + t)
1295
1296 * From the (\t -> t+t) we get type {Num d} => d -> d
1297 where d is fresh.
1298
1299 * Now unify with type of foo's arg, and we get:
1300 {Num (C d a)} => C d a -> C d a
1301 where a is fresh.
1302
1303 * Now abstract over the 'a', but float out the Num (C d a) constraint
1304 because it does not 'really' mention a. (see exactTyVarsOfType)
1305 The arg to foo becomes
1306 \/\a -> \t -> t+t
1307
1308 * So we get a dict binding for Num (C d a), which is zonked to give
1309 a = ()
1310 [Note Sept 04: now that we are zonking quantified type variables
1311 on construction, the 'a' will be frozen as a regular tyvar on
1312 quantification, so the floated dict will still have type (C d a).
1313 Which renders this whole note moot; happily!]
1314
1315 * Then the \/\a abstraction has a zonked 'a' in it.
1316
1317 All very silly. I think its harmless to ignore the problem. We'll end up with
1318 a \/\a in the final result but all the occurrences of a will be zonked to ()
1319
1320 ************************************************************************
1321 * *
1322 Zonking types
1323 * *
1324 ************************************************************************
1325
1326 -}
1327
1328 -- | @tcGetGlobalTyCoVars@ returns a fully-zonked set of *scoped* tyvars free in
1329 -- the environment. To improve subsequent calls to the same function it writes
1330 -- the zonked set back into the environment. Note that this returns all
1331 -- variables free in anything (term-level or type-level) in scope. We thus
1332 -- don't have to worry about clashes with things that are not in scope, because
1333 -- if they are reachable, then they'll be returned here.
1334 -- NB: This is closed over kinds, so it can return unification variables mentioned
1335 -- in the kinds of in-scope tyvars.
1336 tcGetGlobalTyCoVars :: TcM TcTyVarSet
1337 tcGetGlobalTyCoVars
1338 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
1339 ; gbl_tvs <- readMutVar gtv_var
1340 ; gbl_tvs' <- zonkTyCoVarsAndFV gbl_tvs
1341 ; writeMutVar gtv_var gbl_tvs'
1342 ; return gbl_tvs' }
1343
1344 zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
1345 -- Zonk a type and take its free variables
1346 -- With kind polymorphism it can be essential to zonk *first*
1347 -- so that we find the right set of free variables. Eg
1348 -- forall k1. forall (a:k2). a
1349 -- where k2:=k1 is in the substitution. We don't want
1350 -- k2 to look free in this type!
1351 zonkTcTypeAndFV ty
1352 = tyCoVarsOfTypeDSet <$> zonkTcType ty
1353
1354 -- | Zonk a type and call 'candidateQTyVarsOfType' on it.
1355 zonkTcTypeAndSplitDepVars :: TcType -> TcM CandidatesQTvs
1356 zonkTcTypeAndSplitDepVars ty
1357 = candidateQTyVarsOfType <$> zonkTcType ty
1358
1359 zonkTcTypesAndSplitDepVars :: [TcType] -> TcM CandidatesQTvs
1360 zonkTcTypesAndSplitDepVars tys
1361 = candidateQTyVarsOfTypes <$> mapM zonkTcType tys
1362
1363 zonkTyCoVar :: TyCoVar -> TcM TcType
1364 -- Works on TyVars and TcTyVars
1365 zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
1366 | isTyVar tv = mkTyVarTy <$> zonkTyCoVarKind tv
1367 | otherwise = ASSERT2( isCoVar tv, ppr tv )
1368 mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
1369 -- Hackily, when typechecking type and class decls
1370 -- we have TyVars in scopeadded (only) in
1371 -- TcHsType.tcTyClTyVars, but it seems
1372 -- painful to make them into TcTyVars there
1373
1374 zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
1375 zonkTyCoVarsAndFV tycovars =
1376 tyCoVarsOfTypes <$> mapM zonkTyCoVar (nonDetEltsUniqSet tycovars)
1377 -- It's OK to use nonDetEltsUniqSet here because we immediately forget about
1378 -- the ordering by turning it into a nondeterministic set and the order
1379 -- of zonking doesn't matter for determinism.
1380
1381 -- Takes a list of TyCoVars, zonks them and returns a
1382 -- deterministically ordered list of their free variables.
1383 zonkTyCoVarsAndFVList :: [TyCoVar] -> TcM [TyCoVar]
1384 zonkTyCoVarsAndFVList tycovars =
1385 tyCoVarsOfTypesList <$> mapM zonkTyCoVar tycovars
1386
1387 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
1388 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
1389
1390 ----------------- Types
1391 zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
1392 zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
1393 ; return (setTyVarKind tv kind') }
1394
1395 zonkTcTypes :: [TcType] -> TcM [TcType]
1396 zonkTcTypes tys = mapM zonkTcType tys
1397
1398 {-
1399 ************************************************************************
1400 * *
1401 Zonking constraints
1402 * *
1403 ************************************************************************
1404 -}
1405
1406 zonkImplication :: Implication -> TcM Implication
1407 zonkImplication implic@(Implic { ic_skols = skols
1408 , ic_given = given
1409 , ic_wanted = wanted
1410 , ic_info = info })
1411 = do { skols' <- mapM zonkTcTyCoVarBndr skols -- Need to zonk their kinds!
1412 -- as Trac #7230 showed
1413 ; given' <- mapM zonkEvVar given
1414 ; info' <- zonkSkolemInfo info
1415 ; wanted' <- zonkWCRec wanted
1416 ; return (implic { ic_skols = skols'
1417 , ic_given = given'
1418 , ic_wanted = wanted'
1419 , ic_info = info' }) }
1420
1421 zonkEvVar :: EvVar -> TcM EvVar
1422 zonkEvVar var = do { ty' <- zonkTcType (varType var)
1423 ; return (setVarType var ty') }
1424
1425
1426 zonkWC :: WantedConstraints -> TcM WantedConstraints
1427 zonkWC wc = zonkWCRec wc
1428
1429 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
1430 zonkWCRec (WC { wc_simple = simple, wc_impl = implic })
1431 = do { simple' <- zonkSimples simple
1432 ; implic' <- mapBagM zonkImplication implic
1433 ; return (WC { wc_simple = simple', wc_impl = implic' }) }
1434
1435 zonkSimples :: Cts -> TcM Cts
1436 zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
1437 ; traceTc "zonkSimples done:" (ppr cts')
1438 ; return cts' }
1439
1440 zonkCt' :: Ct -> TcM Ct
1441 zonkCt' ct = zonkCt ct
1442
1443 {- Note [zonkCt behaviour]
1444 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1445 zonkCt tries to maintain the canonical form of a Ct. For example,
1446 - a CDictCan should stay a CDictCan;
1447 - a CTyEqCan should stay a CTyEqCan (if the LHS stays as a variable.).
1448 - a CHoleCan should stay a CHoleCan
1449 - a CIrredCan should stay a CIrredCan with its cc_insol flag intact
1450
1451 Why?, for example:
1452 - For CDictCan, the @TcSimplify.expandSuperClasses@ step, which runs after the
1453 simple wanted and plugin loop, looks for @CDictCan@s. If a plugin is in use,
1454 constraints are zonked before being passed to the plugin. This means if we
1455 don't preserve a canonical form, @expandSuperClasses@ fails to expand
1456 superclasses. This is what happened in Trac #11525.
1457
1458 - For CHoleCan, once we forget that it's a hole, we can never recover that info.
1459
1460 - For CIrredCan we want to see if a constraint is insoluble with insolubleWC
1461
1462 NB: we do not expect to see any CFunEqCans, because zonkCt is only
1463 called on unflattened constraints.
1464
1465 NB: Constraints are always re-flattened etc by the canonicaliser in
1466 @TcCanonical@ even if they come in as CDictCan. Only canonical constraints that
1467 are actually in the inert set carry all the guarantees. So it is okay if zonkCt
1468 creates e.g. a CDictCan where the cc_tyars are /not/ function free.
1469 -}
1470
1471 zonkCt :: Ct -> TcM Ct
1472 zonkCt ct@(CHoleCan { cc_ev = ev })
1473 = do { ev' <- zonkCtEvidence ev
1474 ; return $ ct { cc_ev = ev' } }
1475
1476 zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
1477 = do { ev' <- zonkCtEvidence ev
1478 ; args' <- mapM zonkTcType args
1479 ; return $ ct { cc_ev = ev', cc_tyargs = args' } }
1480
1481 zonkCt ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs })
1482 = do { ev' <- zonkCtEvidence ev
1483 ; tv_ty' <- zonkTcTyVar tv
1484 ; case getTyVar_maybe tv_ty' of
1485 Just tv' -> do { rhs' <- zonkTcType rhs
1486 ; return ct { cc_ev = ev'
1487 , cc_tyvar = tv'
1488 , cc_rhs = rhs' } }
1489 Nothing -> return (mkNonCanonical ev') }
1490
1491 zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_insol flag
1492 = do { ev' <- zonkCtEvidence ev
1493 ; return (ct { cc_ev = ev' }) }
1494
1495 zonkCt ct
1496 = ASSERT( not (isCFunEqCan ct) )
1497 -- We do not expect to see any CFunEqCans, because zonkCt is only called on
1498 -- unflattened constraints.
1499 do { fl' <- zonkCtEvidence (ctEvidence ct)
1500 ; return (mkNonCanonical fl') }
1501
1502 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
1503 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
1504 = do { pred' <- zonkTcType pred
1505 ; return (ctev { ctev_pred = pred'}) }
1506 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest })
1507 = do { pred' <- zonkTcType pred
1508 ; let dest' = case dest of
1509 EvVarDest ev -> EvVarDest $ setVarType ev pred'
1510 -- necessary in simplifyInfer
1511 HoleDest h -> HoleDest h
1512 ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
1513 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
1514 = do { pred' <- zonkTcType pred
1515 ; return (ctev { ctev_pred = pred' }) }
1516
1517 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
1518 zonkSkolemInfo (SigSkol cx ty tv_prs) = do { ty' <- zonkTcType ty
1519 ; return (SigSkol cx ty' tv_prs) }
1520 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
1521 ; return (InferSkol ntys') }
1522 where
1523 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
1524 zonkSkolemInfo skol_info = return skol_info
1525
1526 {-
1527 %************************************************************************
1528 %* *
1529 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
1530 * *
1531 * For internal use only! *
1532 * *
1533 ************************************************************************
1534
1535 -}
1536
1537 -- zonkId is used *during* typechecking just to zonk the Id's type
1538 zonkId :: TcId -> TcM TcId
1539 zonkId id
1540 = do { ty' <- zonkTcType (idType id)
1541 ; return (Id.setIdType id ty') }
1542
1543 zonkCoVar :: CoVar -> TcM CoVar
1544 zonkCoVar = zonkId
1545
1546 -- | A suitable TyCoMapper for zonking a type during type-checking,
1547 -- before all metavars are filled in.
1548 zonkTcTypeMapper :: TyCoMapper () TcM
1549 zonkTcTypeMapper = TyCoMapper
1550 { tcm_smart = True
1551 , tcm_tyvar = const zonkTcTyVar
1552 , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
1553 , tcm_hole = hole
1554 , tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv
1555 , tcm_tycon = return }
1556 where
1557 hole :: () -> CoercionHole -> TcM Coercion
1558 hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
1559 = do { contents <- readTcRef ref
1560 ; case contents of
1561 Just co -> do { co' <- zonkCo co
1562 ; checkCoercionHole cv co' }
1563 Nothing -> do { cv' <- zonkCoVar cv
1564 ; return $ HoleCo (hole { ch_co_var = cv' }) } }
1565
1566 -- For unbound, mutable tyvars, zonkType uses the function given to it
1567 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
1568 -- type variable and zonks the kind too
1569 zonkTcType :: TcType -> TcM TcType
1570 zonkTcType = mapType zonkTcTypeMapper ()
1571
1572 -- | "Zonk" a coercion -- really, just zonk any types in the coercion
1573 zonkCo :: Coercion -> TcM Coercion
1574 zonkCo = mapCoercion zonkTcTypeMapper ()
1575
1576 zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
1577 -- A tyvar binder is never a unification variable (TauTv),
1578 -- rather it is always a skolem. It *might* be a TyVarTv.
1579 -- (Because non-CUSK type declarations use TyVarTvs.)
1580 -- Regardless, it may have a kind
1581 -- that has not yet been zonked, and may include kind
1582 -- unification variables.
1583 zonkTcTyCoVarBndr tyvar
1584 | isTyVarTyVar tyvar
1585 = tcGetTyVar "zonkTcTyCoVarBndr TyVarTv" <$> zonkTcTyVar tyvar
1586
1587 | otherwise
1588 -- can't use isCoVar, because it looks at a TyCon. Argh.
1589 = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), pprTyVar tyvar )
1590 updateTyVarKindM zonkTcType tyvar
1591
1592 zonkTcTyVarBinder :: TyVarBndr TcTyVar vis -> TcM (TyVarBndr TcTyVar vis)
1593 zonkTcTyVarBinder (TvBndr tv vis)
1594 = do { tv' <- zonkTcTyCoVarBndr tv
1595 ; return (TvBndr tv' vis) }
1596
1597 zonkTcTyVar :: TcTyVar -> TcM TcType
1598 -- Simply look through all Flexis
1599 zonkTcTyVar tv
1600 | isTcTyVar tv
1601 = case tcTyVarDetails tv of
1602 SkolemTv {} -> zonk_kind_and_return
1603 RuntimeUnk {} -> zonk_kind_and_return
1604 MetaTv { mtv_ref = ref }
1605 -> do { cts <- readMutVar ref
1606 ; case cts of
1607 Flexi -> zonk_kind_and_return
1608 Indirect ty -> zonkTcType ty }
1609
1610 | otherwise -- coercion variable
1611 = zonk_kind_and_return
1612 where
1613 zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv
1614 ; return (mkTyVarTy z_tv) }
1615
1616 -- Variant that assumes that any result of zonking is still a TyVar.
1617 -- Should be used only on skolems and TyVarTvs
1618 zonkTcTyVarToTyVar :: HasDebugCallStack => TcTyVar -> TcM TcTyVar
1619 zonkTcTyVarToTyVar tv
1620 = do { ty <- zonkTcTyVar tv
1621 ; let tv' = case tcGetTyVar_maybe ty of
1622 Just tv' -> tv'
1623 Nothing -> pprPanic "zonkTcTyVarToTyVar"
1624 (ppr tv $$ ppr ty)
1625 ; return tv' }
1626
1627 zonkTyVarTyVarPairs :: [(Name,TcTyVar)] -> TcM [(Name,TcTyVar)]
1628 zonkTyVarTyVarPairs prs
1629 = mapM do_one prs
1630 where
1631 do_one (nm, tv) = do { tv' <- zonkTcTyVarToTyVar tv
1632 ; return (nm, tv') }
1633
1634 {-
1635 %************************************************************************
1636 %* *
1637 Tidying
1638 * *
1639 ************************************************************************
1640 -}
1641
1642 zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
1643 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
1644 ; return (tidyOpenType env ty') }
1645
1646 zonkTidyTcTypes :: TidyEnv -> [TcType] -> TcM (TidyEnv, [TcType])
1647 zonkTidyTcTypes = zonkTidyTcTypes' []
1648 where zonkTidyTcTypes' zs env [] = return (env, reverse zs)
1649 zonkTidyTcTypes' zs env (ty:tys)
1650 = do { (env', ty') <- zonkTidyTcType env ty
1651 ; zonkTidyTcTypes' (ty':zs) env' tys }
1652
1653 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
1654 zonkTidyOrigin env (GivenOrigin skol_info)
1655 = do { skol_info1 <- zonkSkolemInfo skol_info
1656 ; let skol_info2 = tidySkolemInfo env skol_info1
1657 ; return (env, GivenOrigin skol_info2) }
1658 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act
1659 , uo_expected = exp })
1660 = do { (env1, act') <- zonkTidyTcType env act
1661 ; (env2, exp') <- zonkTidyTcType env1 exp
1662 ; return ( env2, orig { uo_actual = act'
1663 , uo_expected = exp' }) }
1664 zonkTidyOrigin env (KindEqOrigin ty1 m_ty2 orig t_or_k)
1665 = do { (env1, ty1') <- zonkTidyTcType env ty1
1666 ; (env2, m_ty2') <- case m_ty2 of
1667 Just ty2 -> second Just <$> zonkTidyTcType env1 ty2
1668 Nothing -> return (env1, Nothing)
1669 ; (env3, orig') <- zonkTidyOrigin env2 orig
1670 ; return (env3, KindEqOrigin ty1' m_ty2' orig' t_or_k) }
1671 zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
1672 = do { (env1, p1') <- zonkTidyTcType env p1
1673 ; (env2, p2') <- zonkTidyTcType env1 p2
1674 ; return (env2, FunDepOrigin1 p1' l1 p2' l2) }
1675 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
1676 = do { (env1, p1') <- zonkTidyTcType env p1
1677 ; (env2, p2') <- zonkTidyTcType env1 p2
1678 ; (env3, o1') <- zonkTidyOrigin env2 o1
1679 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
1680 zonkTidyOrigin env orig = return (env, orig)
1681
1682 ----------------
1683 tidyCt :: TidyEnv -> Ct -> Ct
1684 -- Used only in error reporting
1685 -- Also converts it to non-canonical
1686 tidyCt env ct
1687 = case ct of
1688 CHoleCan { cc_ev = ev }
1689 -> ct { cc_ev = tidy_ev env ev }
1690 _ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
1691 where
1692 tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
1693 -- NB: we do not tidy the ctev_evar field because we don't
1694 -- show it in error messages
1695 tidy_ev env ctev@(CtGiven { ctev_pred = pred })
1696 = ctev { ctev_pred = tidyType env pred }
1697 tidy_ev env ctev@(CtWanted { ctev_pred = pred })
1698 = ctev { ctev_pred = tidyType env pred }
1699 tidy_ev env ctev@(CtDerived { ctev_pred = pred })
1700 = ctev { ctev_pred = tidyType env pred }
1701
1702 ----------------
1703 tidyEvVar :: TidyEnv -> EvVar -> EvVar
1704 tidyEvVar env var = setVarType var (tidyType env (varType var))
1705
1706 ----------------
1707 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
1708 tidySkolemInfo env (DerivSkol ty) = DerivSkol (tidyType env ty)
1709 tidySkolemInfo env (SigSkol cx ty tv_prs) = tidySigSkol env cx ty tv_prs
1710 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
1711 tidySkolemInfo env (UnifyForAllSkol ty) = UnifyForAllSkol (tidyType env ty)
1712 tidySkolemInfo _ info = info
1713
1714 tidySigSkol :: TidyEnv -> UserTypeCtxt
1715 -> TcType -> [(Name,TcTyVar)] -> SkolemInfo
1716 -- We need to take special care when tidying SigSkol
1717 -- See Note [SigSkol SkolemInfo] in TcRnTypes
1718 tidySigSkol env cx ty tv_prs
1719 = SigSkol cx (tidy_ty env ty) tv_prs'
1720 where
1721 tv_prs' = mapSnd (tidyTyVarOcc env) tv_prs
1722 inst_env = mkNameEnv tv_prs'
1723
1724 tidy_ty env (ForAllTy (TvBndr tv vis) ty)
1725 = ForAllTy (TvBndr tv' vis) (tidy_ty env' ty)
1726 where
1727 (env', tv') = tidy_tv_bndr env tv
1728
1729 tidy_ty env (FunTy arg res)
1730 = FunTy (tidyType env arg) (tidy_ty env res)
1731
1732 tidy_ty env ty = tidyType env ty
1733
1734 tidy_tv_bndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
1735 tidy_tv_bndr env@(occ_env, subst) tv
1736 | Just tv' <- lookupNameEnv inst_env (tyVarName tv)
1737 = ((occ_env, extendVarEnv subst tv tv'), tv')
1738
1739 | otherwise
1740 = tidyTyCoVarBndr env tv
1741
1742 -------------------------------------------------------------------------
1743 {-
1744 %************************************************************************
1745 %* *
1746 Levity polymorphism checks
1747 * *
1748 ************************************************************************
1749
1750 See Note [Levity polymorphism checking] in DsMonad
1751
1752 -}
1753
1754 -- | According to the rules around representation polymorphism
1755 -- (see https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds), no binder
1756 -- can have a representation-polymorphic type. This check ensures
1757 -- that we respect this rule. It is a bit regrettable that this error
1758 -- occurs in zonking, after which we should have reported all errors.
1759 -- But it's hard to see where else to do it, because this can be discovered
1760 -- only after all solving is done. And, perhaps most importantly, this
1761 -- isn't really a compositional property of a type system, so it's
1762 -- not a terrible surprise that the check has to go in an awkward spot.
1763 ensureNotLevPoly :: Type -- its zonked type
1764 -> SDoc -- where this happened
1765 -> TcM ()
1766 ensureNotLevPoly ty doc
1767 = whenNoErrs $ -- sometimes we end up zonking bogus definitions of type
1768 -- forall a. a. See, for example, test ghci/scripts/T9140
1769 checkForLevPoly doc ty
1770
1771 -- See Note [Levity polymorphism checking] in DsMonad
1772 checkForLevPoly :: SDoc -> Type -> TcM ()
1773 checkForLevPoly = checkForLevPolyX addErr
1774
1775 checkForLevPolyX :: Monad m
1776 => (SDoc -> m ()) -- how to report an error
1777 -> SDoc -> Type -> m ()
1778 checkForLevPolyX add_err extra ty
1779 | isTypeLevPoly ty
1780 = add_err (formatLevPolyErr ty $$ extra)
1781 | otherwise
1782 = return ()
1783
1784 formatLevPolyErr :: Type -- levity-polymorphic type
1785 -> SDoc
1786 formatLevPolyErr ty
1787 = hang (text "A levity-polymorphic type is not allowed here:")
1788 2 (vcat [ text "Type:" <+> pprWithTYPE tidy_ty
1789 , text "Kind:" <+> pprWithTYPE tidy_ki ])
1790 where
1791 (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty
1792 tidy_ki = tidyType tidy_env (typeKind ty)