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