Small refactoring of meta-tyvar cloning
[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 newSigTyVar :: Name -> Kind -> TcM TcTyVar
584 newSigTyVar name kind
585 = do { details <- newMetaDetails SigTv
586 ; return (mkTcTyVar name kind details) }
587
588 newFmvTyVar :: TcType -> TcM TcTyVar
589 -- Very like newMetaTyVar, except sets mtv_tclvl to one less
590 -- so that the fmv is untouchable.
591 newFmvTyVar fam_ty
592 = do { uniq <- newUnique
593 ; ref <- newMutVar Flexi
594 ; let details = MetaTv { mtv_info = FlatMetaTv
595 , mtv_ref = ref
596 , mtv_tclvl = fmvTcLevel }
597 name = mkMetaTyVarName uniq (fsLit "s")
598 ; return (mkTcTyVar name (typeKind fam_ty) details) }
599
600 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
601 newMetaDetails info
602 = do { ref <- newMutVar Flexi
603 ; tclvl <- getTcLevel
604 ; return (MetaTv { mtv_info = info
605 , mtv_ref = ref
606 , mtv_tclvl = tclvl }) }
607
608 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
609 cloneMetaTyVar tv
610 = ASSERT( isTcTyVar tv )
611 do { uniq <- newUnique
612 ; ref <- newMutVar Flexi
613 ; let name' = setNameUnique (tyVarName tv) uniq
614 details' = case tcTyVarDetails tv of
615 details@(MetaTv {}) -> details { mtv_ref = ref }
616 _ -> pprPanic "cloneMetaTyVar" (ppr tv)
617 ; return (mkTcTyVar name' (tyVarKind tv) details') }
618
619 -- Works for both type and kind variables
620 readMetaTyVar :: TyVar -> TcM MetaDetails
621 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
622 readMutVar (metaTyVarRef tyvar)
623
624 isFilledMetaTyVar :: TyVar -> TcM Bool
625 -- True of a filled-in (Indirect) meta type variable
626 isFilledMetaTyVar tv
627 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
628 = do { details <- readMutVar ref
629 ; return (isIndirect details) }
630 | otherwise = return False
631
632 isUnfilledMetaTyVar :: TyVar -> TcM Bool
633 -- True of a un-filled-in (Flexi) meta type variable
634 isUnfilledMetaTyVar tv
635 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
636 = do { details <- readMutVar ref
637 ; return (isFlexi details) }
638 | otherwise = return False
639
640 --------------------
641 -- Works with both type and kind variables
642 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
643 -- Write into a currently-empty MetaTyVar
644
645 writeMetaTyVar tyvar ty
646 | not debugIsOn
647 = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty
648
649 -- Everything from here on only happens if DEBUG is on
650 | not (isTcTyVar tyvar)
651 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
652 return ()
653
654 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
655 = writeMetaTyVarRef tyvar ref ty
656
657 | otherwise
658 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
659 return ()
660
661 --------------------
662 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
663 -- Here the tyvar is for error checking only;
664 -- the ref cell must be for the same tyvar
665 writeMetaTyVarRef tyvar ref ty
666 | not debugIsOn
667 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
668 <+> text ":=" <+> ppr ty)
669 ; writeTcRef ref (Indirect ty) }
670
671 -- Everything from here on only happens if DEBUG is on
672 | otherwise
673 = do { meta_details <- readMutVar ref;
674 -- Zonk kinds to allow the error check to work
675 ; zonked_tv_kind <- zonkTcType tv_kind
676 ; zonked_ty_kind <- zonkTcType ty_kind
677 ; let kind_check_ok = isPredTy tv_kind -- Don't check kinds for updates
678 -- to coercion variables
679 || tcEqKind zonked_ty_kind zonked_tv_kind
680
681 kind_msg = hang (text "Ill-kinded update to meta tyvar")
682 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
683 <+> text ":="
684 <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) )
685
686 ; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
687
688 -- Check for double updates
689 ; MASSERT2( isFlexi meta_details, double_upd_msg meta_details )
690
691 -- Check for level OK
692 -- See Note [Level check when unifying]
693 ; MASSERT2( level_check_ok, level_check_msg )
694
695 -- Check Kinds ok
696 ; MASSERT2( kind_check_ok, kind_msg )
697
698 -- Do the write
699 ; writeMutVar ref (Indirect ty) }
700 where
701 tv_kind = tyVarKind tyvar
702 ty_kind = typeKind ty
703
704 tv_lvl = tcTyVarLevel tyvar
705 ty_lvl = tcTypeLevel ty
706
707 level_check_ok = isFlattenTyVar tyvar
708 || not (ty_lvl `strictlyDeeperThan` tv_lvl)
709 level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
710
711 double_upd_msg details = hang (text "Double update of meta tyvar")
712 2 (ppr tyvar $$ ppr details)
713
714
715 {- Note [Level check when unifying]
716 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
717 When unifying
718 alpha:lvl := ty
719 we expect that the TcLevel of 'ty' will be <= lvl.
720 However, during unflatting we do
721 fuv:l := ty:(l+1)
722 which is usually wrong; hence the check isFmmvTyVar in level_check_ok.
723 See Note [TcLevel assignment] in TcType.
724 -}
725
726 {-
727 % Generating fresh variables for pattern match check
728 -}
729
730 -- UNINSTANTIATED VERSION OF tcInstSkolTyCoVars
731 genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar]
732 -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
733 -- Precondition: tyvars should be scoping-ordered
734 -- see Note [Kind substitution when instantiating]
735 -- Get the location from the monad; this is a complete freshening operation
736 genInstSkolTyVarsX loc subst tvs
737 = instSkolTyCoVarsX (mkTcSkolTyVar topTcLevel loc False) subst tvs
738
739 {-
740 ************************************************************************
741 * *
742 MetaTvs: TauTvs
743 * *
744 ************************************************************************
745
746 Note [Never need to instantiate coercion variables]
747 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
748 With coercion variables sloshing around in types, it might seem that we
749 sometimes need to instantiate coercion variables. This would be problematic,
750 because coercion variables inhabit unboxed equality (~#), and the constraint
751 solver thinks in terms only of boxed equality (~). The solution is that
752 we never need to instantiate coercion variables in the first place.
753
754 The tyvars that we need to instantiate come from the types of functions,
755 data constructors, and patterns. These will never be quantified over
756 coercion variables, except for the special case of the promoted Eq#. But,
757 that can't ever appear in user code, so we're safe!
758 -}
759
760 mkMetaTyVarName :: Unique -> FastString -> Name
761 -- Makes a /System/ Name, which is eagerly eliminated by
762 -- the unifier; see TcUnify.nicer_to_update_tv1, and
763 -- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
764 mkMetaTyVarName uniq str = mkSystemName uniq (mkTyVarOccFS str)
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 cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
780 -- Same as newAnonMetaTyVar, but use a supplied TyVar as the source of the print-name
781 cloneAnonMetaTyVar info tv kind
782 = do { uniq <- newUnique
783 ; details <- newMetaDetails info
784 ; let name = mkSystemName uniq (getOccName tv)
785 -- See Note [Name of an instantiated type variable]
786 ; return (mkTcTyVar name kind details) }
787
788 {- Note [Name of an instantiated type variable]
789 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
790 At the moment we give a unification variable a System Name, which
791 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
792 -}
793
794 newFlexiTyVar :: Kind -> TcM TcTyVar
795 newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
796
797 newFlexiTyVarTy :: Kind -> TcM TcType
798 newFlexiTyVarTy kind = do
799 tc_tyvar <- newFlexiTyVar kind
800 return (mkTyVarTy tc_tyvar)
801
802 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
803 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
804
805 newOpenTypeKind :: TcM TcKind
806 newOpenTypeKind
807 = do { rr <- newFlexiTyVarTy runtimeRepTy
808 ; return (tYPE rr) }
809
810 -- | Create a tyvar that can be a lifted or unlifted type.
811 -- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh
812 newOpenFlexiTyVarTy :: TcM TcType
813 newOpenFlexiTyVarTy
814 = do { kind <- newOpenTypeKind
815 ; newFlexiTyVarTy kind }
816
817 newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
818 newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
819
820 newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
821 -- Instantiate with META type variables
822 -- Note that this works for a sequence of kind, type, and coercion variables
823 -- variables. Eg [ (k:*), (a:k->k) ]
824 -- Gives [ (k7:*), (a8:k7->k7) ]
825 newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
826 -- emptyTCvSubst has an empty in-scope set, but that's fine here
827 -- Since the tyvars are freshly made, they cannot possibly be
828 -- captured by any existing for-alls.
829
830 newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
831 -- Make a new unification variable tyvar whose Name and Kind come from
832 -- an existing TyVar. We substitute kind variables in the kind.
833 newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
834
835 newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
836 -- Just like newMetaTyVars, but start with an existing substitution.
837 newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
838
839 newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
840 -- Just like newMetaTyVarX, but make a SigTv
841 newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar
842
843 newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
844 newWildCardX subst tv
845 = do { new_tv <- newAnonMetaTyVar TauTv (substTy subst (tyVarKind tv))
846 ; return (extendTvSubstWithClone subst tv new_tv, new_tv) }
847
848 new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
849 new_meta_tv_x info subst tv
850 = do { new_tv <- cloneAnonMetaTyVar info tv substd_kind
851 ; let subst1 = extendTvSubstWithClone subst tv new_tv
852 ; return (subst1, new_tv) }
853 where
854 substd_kind = substTyUnchecked subst (tyVarKind tv)
855 -- NOTE: Trac #12549 is fixed so we could use
856 -- substTy here, but the tc_infer_args problem
857 -- is not yet fixed so leaving as unchecked for now.
858 -- OLD NOTE:
859 -- Unchecked because we call newMetaTyVarX from
860 -- tcInstBinder, which is called from tc_infer_args
861 -- which does not yet take enough trouble to ensure
862 -- the in-scope set is right; e.g. Trac #12785 trips
863 -- if we use substTy here
864
865 newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
866 newMetaTyVarTyAtLevel tc_lvl kind
867 = do { uniq <- newUnique
868 ; ref <- newMutVar Flexi
869 ; let name = mkMetaTyVarName uniq (fsLit "p")
870 details = MetaTv { mtv_info = TauTv
871 , mtv_ref = ref
872 , mtv_tclvl = tc_lvl }
873 ; return (mkTyVarTy (mkTcTyVar name kind details)) }
874
875 {- *********************************************************************
876 * *
877 Quantification
878 * *
879 ************************************************************************
880
881 Note [quantifyTyVars]
882 ~~~~~~~~~~~~~~~~~~~~~
883 quantifyTyVars is given the free vars of a type that we
884 are about to wrap in a forall.
885
886 It takes these free type/kind variables (partitioned into dependent and
887 non-dependent variables) and
888 1. Zonks them and remove globals and covars
889 2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
890 3. Calls zonkQuantifiedTyVar on each
891
892 Step (2) is often unimportant, because the kind variable is often
893 also free in the type. Eg
894 Typeable k (a::k)
895 has free vars {k,a}. But the type (see Trac #7916)
896 (f::k->*) (a::k)
897 has free vars {f,a}, but we must add 'k' as well! Hence step (3).
898
899 * This function distinguishes between dependent and non-dependent
900 variables only to keep correct defaulting behavior with -XNoPolyKinds.
901 With -XPolyKinds, it treats both classes of variables identically.
902
903 * quantifyTyVars never quantifies over
904 - a coercion variable
905 - a runtime-rep variable
906
907 Note [quantifyTyVars determinism]
908 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
909 The results of quantifyTyVars are wrapped in a forall and can end up in the
910 interface file. One such example is inferred type signatures. They also affect
911 the results of optimizations, for example worker-wrapper. This means that to
912 get deterministic builds quantifyTyVars needs to be deterministic.
913
914 To achieve this CandidatesQTvs is backed by deterministic sets which allows them
915 to be later converted to a list in a deterministic order.
916
917 For more information about deterministic sets see
918 Note [Deterministic UniqFM] in UniqDFM.
919 -}
920
921 quantifyTyVars
922 :: TcTyCoVarSet -- Global tvs; already zonked
923 -> CandidatesQTvs -- See Note [Dependent type variables] in TcType
924 -- Already zonked
925 -> TcM [TcTyVar]
926 -- See Note [quantifyTyVars]
927 -- Can be given a mixture of TcTyVars and TyVars, in the case of
928 -- associated type declarations. Also accepts covars, but *never* returns any.
929
930 quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
931 = do { traceTc "quantifyTyVars" (vcat [ppr dvs, ppr gbl_tvs])
932 ; let all_cvs = filterVarSet isCoVar $ dVarSetToVarSet dep_tkvs
933 dep_kvs = dVarSetElemsWellScoped $
934 dep_tkvs `dVarSetMinusVarSet` gbl_tvs
935 `dVarSetMinusVarSet` closeOverKinds all_cvs
936 -- dVarSetElemsWellScoped: put the kind variables into
937 -- well-scoped order.
938 -- E.g. [k, (a::k)] not the other way roud
939 -- closeOverKinds all_cvs: do not quantify over coercion
940 -- variables, or any any tvs that a covar depends on
941
942 nondep_tvs = dVarSetElems $
943 (nondep_tkvs `minusDVarSet` dep_tkvs)
944 `dVarSetMinusVarSet` gbl_tvs
945 -- See Note [Dependent type variables] in TcType
946 -- The `minus` dep_tkvs removes any kind-level vars
947 -- e.g. T k (a::k) Since k appear in a kind it'll
948 -- be in dv_kvs, and is dependent. So remove it from
949 -- dv_tvs which will also contain k
950 -- No worry about dependent covars here;
951 -- they are all in dep_tkvs
952 -- No worry about scoping, because these are all
953 -- type variables
954 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
955
956 -- In the non-PolyKinds case, default the kind variables
957 -- to *, and zonk the tyvars as usual. Notice that this
958 -- may make quantifyTyVars return a shorter list
959 -- than it was passed, but that's ok
960 ; poly_kinds <- xoptM LangExt.PolyKinds
961 ; dep_kvs' <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs
962 ; nondep_tvs' <- mapMaybeM (zonk_quant False) nondep_tvs
963 -- Because of the order, any kind variables
964 -- mentioned in the kinds of the nondep_tvs'
965 -- now refer to the dep_kvs'
966
967 ; traceTc "quantifyTyVars"
968 (vcat [ text "globals:" <+> ppr gbl_tvs
969 , text "nondep:" <+> pprTyVars nondep_tvs
970 , text "dep:" <+> pprTyVars dep_kvs
971 , text "dep_kvs'" <+> pprTyVars dep_kvs'
972 , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ])
973
974 ; return (dep_kvs' ++ nondep_tvs') }
975 where
976 -- zonk_quant returns a tyvar if it should be quantified over;
977 -- otherwise, it returns Nothing. The latter case happens for
978 -- * Kind variables, with -XNoPolyKinds: don't quantify over these
979 -- * RuntimeRep variables: we never quantify over these
980 zonk_quant default_kind tkv
981 | not (isTcTyVar tkv)
982 = return (Just tkv) -- For associated types, we have the class variables
983 -- in scope, and they are TyVars not TcTyVars
984 | otherwise
985 = do { deflt_done <- defaultTyVar default_kind tkv
986 ; case deflt_done of
987 True -> return Nothing
988 False -> do { tv <- zonkQuantifiedTyVar tkv
989 ; return (Just tv) } }
990
991 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
992 -- The quantified type variables often include meta type variables
993 -- we want to freeze them into ordinary type variables
994 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
995 -- bound occurrences of the original type variable will get zonked to
996 -- the immutable version.
997 --
998 -- We leave skolem TyVars alone; they are immutable.
999 --
1000 -- This function is called on both kind and type variables,
1001 -- but kind variables *only* if PolyKinds is on.
1002
1003 zonkQuantifiedTyVar tv
1004 = case tcTyVarDetails tv of
1005 SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
1006 ; return (setTyVarKind tv kind) }
1007 -- It might be a skolem type variable,
1008 -- for example from a user type signature
1009
1010 MetaTv {} -> skolemiseUnboundMetaTyVar tv
1011
1012 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- RuntimeUnk
1013
1014 defaultTyVar :: Bool -- True <=> please default this kind variable to *
1015 -> TcTyVar -- If it's a MetaTyVar then it is unbound
1016 -> TcM Bool -- True <=> defaulted away altogether
1017
1018 defaultTyVar default_kind tv
1019 | not (isMetaTyVar tv)
1020 = return False
1021
1022 | isRuntimeRepVar tv && not_sig_tv -- We never quantify over a RuntimeRep var
1023 = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
1024 ; writeMetaTyVar tv liftedRepTy
1025 ; return True }
1026
1027 | default_kind && not_sig_tv -- -XNoPolyKinds and this is a kind var
1028 = do { default_kind_var tv -- so default it to * if possible
1029 ; return True }
1030
1031 | otherwise
1032 = return False
1033
1034 where
1035 -- Do not default SigTvs. Doing so would violate the invariants
1036 -- on SigTvs; see Note [Signature skolems] in TcType.
1037 -- Trac #13343 is an example
1038 not_sig_tv = not (isSigTyVar tv)
1039
1040 default_kind_var :: TyVar -> TcM ()
1041 -- defaultKindVar is used exclusively with -XNoPolyKinds
1042 -- See Note [Defaulting with -XNoPolyKinds]
1043 -- It takes an (unconstrained) meta tyvar and defaults it.
1044 -- Works only on vars of type *; for other kinds, it issues an error.
1045 default_kind_var kv
1046 | isStarKind (tyVarKind kv)
1047 = do { traceTc "Defaulting a kind var to *" (ppr kv)
1048 ; writeMetaTyVar kv liftedTypeKind }
1049 | otherwise
1050 = addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
1051 , text "of kind:" <+> ppr (tyVarKind kv')
1052 , text "Perhaps enable PolyKinds or add a kind signature" ])
1053 where
1054 (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
1055
1056 skolemiseRuntimeUnk :: TcTyVar -> TcM TyVar
1057 skolemiseRuntimeUnk tv
1058 = skolemise_tv tv RuntimeUnk
1059
1060 skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar
1061 skolemiseUnboundMetaTyVar tv
1062 = skolemise_tv tv (SkolemTv (metaTyVarTcLevel tv) False)
1063
1064 skolemise_tv :: TcTyVar -> TcTyVarDetails -> TcM TyVar
1065 -- We have a Meta tyvar with a ref-cell inside it
1066 -- Skolemise it, so that
1067 -- we are totally out of Meta-tyvar-land
1068 -- We create a skolem TyVar, not a regular TyVar
1069 -- See Note [Zonking to Skolem]
1070 skolemise_tv tv details
1071 = ASSERT2( isMetaTyVar tv, ppr tv )
1072 do { when debugIsOn (check_empty tv)
1073 ; span <- getSrcSpanM -- Get the location from "here"
1074 -- ie where we are generalising
1075 ; kind <- zonkTcType (tyVarKind tv)
1076 ; let uniq = getUnique tv
1077 -- NB: Use same Unique as original tyvar. This is
1078 -- important for TcHsType.splitTelescopeTvs to work properly
1079
1080 tv_name = getOccName tv
1081 final_name = mkInternalName uniq tv_name span
1082 final_tv = mkTcTyVar final_name kind details
1083
1084 ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
1085 ; writeMetaTyVar tv (mkTyVarTy final_tv)
1086 ; return final_tv }
1087
1088 where
1089 check_empty tv -- [Sept 04] Check for non-empty.
1090 = when debugIsOn $ -- See note [Silly Type Synonym]
1091 do { cts <- readMetaTyVar tv
1092 ; case cts of
1093 Flexi -> return ()
1094 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
1095 return () }
1096
1097 {- Note [Defaulting with -XNoPolyKinds]
1098 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1099 Consider
1100
1101 data Compose f g a = Mk (f (g a))
1102
1103 We infer
1104
1105 Compose :: forall k1 k2. (k2 -> *) -> (k1 -> k2) -> k1 -> *
1106 Mk :: forall k1 k2 (f :: k2 -> *) (g :: k1 -> k2) (a :: k1).
1107 f (g a) -> Compose k1 k2 f g a
1108
1109 Now, in another module, we have -XNoPolyKinds -XDataKinds in effect.
1110 What does 'Mk mean? Pre GHC-8.0 with -XNoPolyKinds,
1111 we just defaulted all kind variables to *. But that's no good here,
1112 because the kind variables in 'Mk aren't of kind *, so defaulting to *
1113 is ill-kinded.
1114
1115 After some debate on #11334, we decided to issue an error in this case.
1116 The code is in defaultKindVar.
1117
1118 Note [What is a meta variable?]
1119 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1120 A "meta type-variable", also know as a "unification variable" is a placeholder
1121 introduced by the typechecker for an as-yet-unknown monotype.
1122
1123 For example, when we see a call `reverse (f xs)`, we know that we calling
1124 reverse :: forall a. [a] -> [a]
1125 So we know that the argument `f xs` must be a "list of something". But what is
1126 the "something"? We don't know until we explore the `f xs` a bit more. So we set
1127 out what we do know at the call of `reverse` by instantiate its type with a fresh
1128 meta tyvar, `alpha` say. So now the type of the argument `f xs`, and of the
1129 result, is `[alpha]`. The unification variable `alpha` stands for the
1130 as-yet-unknown type of the elements of the list.
1131
1132 As type inference progresses we may learn more about `alpha`. For example, suppose
1133 `f` has the type
1134 f :: forall b. b -> [Maybe b]
1135 Then we instantiate `f`'s type with another fresh unification variable, say
1136 `beta`; and equate `f`'s result type with reverse's argument type, thus
1137 `[alpha] ~ [Maybe beta]`.
1138
1139 Now we can solve this equality to learn that `alpha ~ Maybe beta`, so we've
1140 refined our knowledge about `alpha`. And so on.
1141
1142 If you found this Note useful, you may also want to have a look at
1143 Section 5 of "Practical type inference for higher rank types" (Peyton Jones,
1144 Vytiniotis, Weirich and Shields. J. Functional Programming. 2011).
1145
1146 Note [What is zonking?]
1147 ~~~~~~~~~~~~~~~~~~~~~~~
1148 GHC relies heavily on mutability in the typechecker for efficient operation.
1149 For this reason, throughout much of the type checking process meta type
1150 variables (the MetaTv constructor of TcTyVarDetails) are represented by mutable
1151 variables (known as TcRefs).
1152
1153 Zonking is the process of ripping out these mutable variables and replacing them
1154 with a real Type. This involves traversing the entire type expression, but the
1155 interesting part of replacing the mutable variables occurs in zonkTyVarOcc.
1156
1157 There are two ways to zonk a Type:
1158
1159 * zonkTcTypeToType, which is intended to be used at the end of type-checking
1160 for the final zonk. It has to deal with unfilled metavars, either by filling
1161 it with a value like Any or failing (determined by the UnboundTyVarZonker
1162 used).
1163
1164 * zonkTcType, which will happily ignore unfilled metavars. This is the
1165 appropriate function to use while in the middle of type-checking.
1166
1167 Note [Zonking to Skolem]
1168 ~~~~~~~~~~~~~~~~~~~~~~~~
1169 We used to zonk quantified type variables to regular TyVars. However, this
1170 leads to problems. Consider this program from the regression test suite:
1171
1172 eval :: Int -> String -> String -> String
1173 eval 0 root actual = evalRHS 0 root actual
1174
1175 evalRHS :: Int -> a
1176 evalRHS 0 root actual = eval 0 root actual
1177
1178 It leads to the deferral of an equality (wrapped in an implication constraint)
1179
1180 forall a. () => ((String -> String -> String) ~ a)
1181
1182 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
1183 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
1184 This has the *side effect* of also zonking the `a' in the deferred equality
1185 (which at this point is being handed around wrapped in an implication
1186 constraint).
1187
1188 Finally, the equality (with the zonked `a') will be handed back to the
1189 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
1190 If we zonk `a' with a regular type variable, we will have this regular type
1191 variable now floating around in the simplifier, which in many places assumes to
1192 only see proper TcTyVars.
1193
1194 We can avoid this problem by zonking with a skolem. The skolem is rigid
1195 (which we require for a quantified variable), but is still a TcTyVar that the
1196 simplifier knows how to deal with.
1197
1198 Note [Silly Type Synonyms]
1199 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1200 Consider this:
1201 type C u a = u -- Note 'a' unused
1202
1203 foo :: (forall a. C u a -> C u a) -> u
1204 foo x = ...
1205
1206 bar :: Num u => u
1207 bar = foo (\t -> t + t)
1208
1209 * From the (\t -> t+t) we get type {Num d} => d -> d
1210 where d is fresh.
1211
1212 * Now unify with type of foo's arg, and we get:
1213 {Num (C d a)} => C d a -> C d a
1214 where a is fresh.
1215
1216 * Now abstract over the 'a', but float out the Num (C d a) constraint
1217 because it does not 'really' mention a. (see exactTyVarsOfType)
1218 The arg to foo becomes
1219 \/\a -> \t -> t+t
1220
1221 * So we get a dict binding for Num (C d a), which is zonked to give
1222 a = ()
1223 [Note Sept 04: now that we are zonking quantified type variables
1224 on construction, the 'a' will be frozen as a regular tyvar on
1225 quantification, so the floated dict will still have type (C d a).
1226 Which renders this whole note moot; happily!]
1227
1228 * Then the \/\a abstraction has a zonked 'a' in it.
1229
1230 All very silly. I think its harmless to ignore the problem. We'll end up with
1231 a \/\a in the final result but all the occurrences of a will be zonked to ()
1232
1233 ************************************************************************
1234 * *
1235 Zonking types
1236 * *
1237 ************************************************************************
1238
1239 -}
1240
1241 -- | @tcGetGlobalTyCoVars@ returns a fully-zonked set of *scoped* tyvars free in
1242 -- the environment. To improve subsequent calls to the same function it writes
1243 -- the zonked set back into the environment. Note that this returns all
1244 -- variables free in anything (term-level or type-level) in scope. We thus
1245 -- don't have to worry about clashes with things that are not in scope, because
1246 -- if they are reachable, then they'll be returned here.
1247 tcGetGlobalTyCoVars :: TcM TcTyVarSet
1248 tcGetGlobalTyCoVars
1249 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
1250 ; gbl_tvs <- readMutVar gtv_var
1251 ; gbl_tvs' <- zonkTyCoVarsAndFV gbl_tvs
1252 ; writeMutVar gtv_var gbl_tvs'
1253 ; return gbl_tvs' }
1254
1255 -- | Zonk a type without using the smart constructors; the result type
1256 -- is available for inspection within the type-checking knot.
1257 zonkTcTypeInKnot :: TcType -> TcM TcType
1258 zonkTcTypeInKnot = mapType (zonkTcTypeMapper { tcm_smart = False }) ()
1259
1260 zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
1261 -- Zonk a type and take its free variables
1262 -- With kind polymorphism it can be essential to zonk *first*
1263 -- so that we find the right set of free variables. Eg
1264 -- forall k1. forall (a:k2). a
1265 -- where k2:=k1 is in the substitution. We don't want
1266 -- k2 to look free in this type!
1267 -- NB: This might be called from within the knot, so don't use
1268 -- smart constructors. See Note [Zonking within the knot] in TcHsType
1269 zonkTcTypeAndFV ty
1270 = tyCoVarsOfTypeDSet <$> zonkTcTypeInKnot ty
1271
1272 -- | Zonk a type and call 'candidateQTyVarsOfType' on it.
1273 -- Works within the knot.
1274 zonkTcTypeAndSplitDepVars :: TcType -> TcM CandidatesQTvs
1275 zonkTcTypeAndSplitDepVars ty
1276 = candidateQTyVarsOfType <$> zonkTcTypeInKnot ty
1277
1278 zonkTcTypesAndSplitDepVars :: [TcType] -> TcM CandidatesQTvs
1279 zonkTcTypesAndSplitDepVars tys
1280 = candidateQTyVarsOfTypes <$> mapM zonkTcTypeInKnot tys
1281
1282 zonkTyCoVar :: TyCoVar -> TcM TcType
1283 -- Works on TyVars and TcTyVars
1284 zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
1285 | isTyVar tv = mkTyVarTy <$> zonkTyCoVarKind tv
1286 | otherwise = ASSERT2( isCoVar tv, ppr tv )
1287 mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
1288 -- Hackily, when typechecking type and class decls
1289 -- we have TyVars in scopeadded (only) in
1290 -- TcHsType.tcTyClTyVars, but it seems
1291 -- painful to make them into TcTyVars there
1292
1293 zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
1294 zonkTyCoVarsAndFV tycovars =
1295 tyCoVarsOfTypes <$> mapM zonkTyCoVar (nonDetEltsUniqSet tycovars)
1296 -- It's OK to use nonDetEltsUniqSet here because we immediately forget about
1297 -- the ordering by turning it into a nondeterministic set and the order
1298 -- of zonking doesn't matter for determinism.
1299
1300 -- Takes a list of TyCoVars, zonks them and returns a
1301 -- deterministically ordered list of their free variables.
1302 zonkTyCoVarsAndFVList :: [TyCoVar] -> TcM [TyCoVar]
1303 zonkTyCoVarsAndFVList tycovars =
1304 tyCoVarsOfTypesList <$> mapM zonkTyCoVar tycovars
1305
1306 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
1307 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
1308
1309 ----------------- Types
1310 zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
1311 zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
1312 ; return (setTyVarKind tv kind') }
1313
1314 zonkTcTypes :: [TcType] -> TcM [TcType]
1315 zonkTcTypes tys = mapM zonkTcType tys
1316
1317 {-
1318 ************************************************************************
1319 * *
1320 Zonking constraints
1321 * *
1322 ************************************************************************
1323 -}
1324
1325 zonkImplication :: Implication -> TcM Implication
1326 zonkImplication implic@(Implic { ic_skols = skols
1327 , ic_given = given
1328 , ic_wanted = wanted
1329 , ic_info = info })
1330 = do { skols' <- mapM zonkTcTyCoVarBndr skols -- Need to zonk their kinds!
1331 -- as Trac #7230 showed
1332 ; given' <- mapM zonkEvVar given
1333 ; info' <- zonkSkolemInfo info
1334 ; wanted' <- zonkWCRec wanted
1335 ; return (implic { ic_skols = skols'
1336 , ic_given = given'
1337 , ic_wanted = wanted'
1338 , ic_info = info' }) }
1339
1340 zonkEvVar :: EvVar -> TcM EvVar
1341 zonkEvVar var = do { ty' <- zonkTcType (varType var)
1342 ; return (setVarType var ty') }
1343
1344
1345 zonkWC :: WantedConstraints -> TcM WantedConstraints
1346 zonkWC wc = zonkWCRec wc
1347
1348 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
1349 zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
1350 = do { simple' <- zonkSimples simple
1351 ; implic' <- mapBagM zonkImplication implic
1352 ; insol' <- zonkSimples insol
1353 ; return (WC { wc_simple = simple', wc_impl = implic', wc_insol = insol' }) }
1354
1355 zonkSimples :: Cts -> TcM Cts
1356 zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
1357 ; traceTc "zonkSimples done:" (ppr cts')
1358 ; return cts' }
1359
1360 zonkCt' :: Ct -> TcM Ct
1361 zonkCt' ct = zonkCt ct
1362
1363 {- Note [zonkCt behaviour]
1364 zonkCt tries to maintain the canonical form of a Ct. For example,
1365 - a CDictCan should stay a CDictCan;
1366 - a CTyEqCan should stay a CTyEqCan (if the LHS stays as a variable.).
1367 - a CHoleCan should stay a CHoleCan
1368
1369 Why?, for example:
1370 - For CDictCan, the @TcSimplify.expandSuperClasses@ step, which runs after the
1371 simple wanted and plugin loop, looks for @CDictCan@s. If a plugin is in use,
1372 constraints are zonked before being passed to the plugin. This means if we
1373 don't preserve a canonical form, @expandSuperClasses@ fails to expand
1374 superclasses. This is what happened in Trac #11525.
1375
1376 - For CHoleCan, once we forget that it's a hole, we can never recover that info.
1377
1378 NB: we do not expect to see any CFunEqCans, because zonkCt is only
1379 called on unflattened constraints.
1380 NB: Constraints are always re-flattened etc by the canonicaliser in
1381 @TcCanonical@ even if they come in as CDictCan. Only canonical constraints that
1382 are actually in the inert set carry all the guarantees. So it is okay if zonkCt
1383 creates e.g. a CDictCan where the cc_tyars are /not/ function free.
1384 -}
1385 zonkCt :: Ct -> TcM Ct
1386 zonkCt ct@(CHoleCan { cc_ev = ev })
1387 = do { ev' <- zonkCtEvidence ev
1388 ; return $ ct { cc_ev = ev' } }
1389 zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
1390 = do { ev' <- zonkCtEvidence ev
1391 ; args' <- mapM zonkTcType args
1392 ; return $ ct { cc_ev = ev', cc_tyargs = args' } }
1393 zonkCt ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs })
1394 = do { ev' <- zonkCtEvidence ev
1395 ; tv_ty' <- zonkTcTyVar tv
1396 ; case getTyVar_maybe tv_ty' of
1397 Just tv' -> do { rhs' <- zonkTcType rhs
1398 ; return ct { cc_ev = ev'
1399 , cc_tyvar = tv'
1400 , cc_rhs = rhs' } }
1401 Nothing -> return (mkNonCanonical ev') }
1402 zonkCt ct
1403 = ASSERT( not (isCFunEqCan ct) )
1404 -- We do not expect to see any CFunEqCans, because zonkCt is only called on
1405 -- unflattened constraints.
1406 do { fl' <- zonkCtEvidence (cc_ev ct)
1407 ; return (mkNonCanonical fl') }
1408
1409 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
1410 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
1411 = do { pred' <- zonkTcType pred
1412 ; return (ctev { ctev_pred = pred'}) }
1413 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest })
1414 = do { pred' <- zonkTcType pred
1415 ; let dest' = case dest of
1416 EvVarDest ev -> EvVarDest $ setVarType ev pred'
1417 -- necessary in simplifyInfer
1418 HoleDest h -> HoleDest h
1419 ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
1420 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
1421 = do { pred' <- zonkTcType pred
1422 ; return (ctev { ctev_pred = pred' }) }
1423
1424 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
1425 zonkSkolemInfo (SigSkol cx ty tv_prs) = do { ty' <- zonkTcType ty
1426 ; return (SigSkol cx ty' tv_prs) }
1427 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
1428 ; return (InferSkol ntys') }
1429 where
1430 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
1431 zonkSkolemInfo skol_info = return skol_info
1432
1433 {-
1434 %************************************************************************
1435 %* *
1436 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
1437 * *
1438 * For internal use only! *
1439 * *
1440 ************************************************************************
1441
1442 -}
1443
1444 -- zonkId is used *during* typechecking just to zonk the Id's type
1445 zonkId :: TcId -> TcM TcId
1446 zonkId id
1447 = do { ty' <- zonkTcType (idType id)
1448 ; return (Id.setIdType id ty') }
1449
1450 -- | A suitable TyCoMapper for zonking a type inside the knot, and
1451 -- before all metavars are filled in.
1452 zonkTcTypeMapper :: TyCoMapper () TcM
1453 zonkTcTypeMapper = TyCoMapper
1454 { tcm_smart = True
1455 , tcm_tyvar = const zonkTcTyVar
1456 , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
1457 , tcm_hole = hole
1458 , tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv }
1459 where
1460 hole :: () -> CoercionHole -> Role -> Type -> Type
1461 -> TcM Coercion
1462 hole _ h r t1 t2
1463 = do { contents <- unpackCoercionHole_maybe h
1464 ; case contents of
1465 Just co -> do { co <- zonkCo co
1466 ; checkCoercionHole co h r t1 t2 }
1467 Nothing -> do { t1 <- zonkTcType t1
1468 ; t2 <- zonkTcType t2
1469 ; return $ mkHoleCo h r t1 t2 } }
1470
1471
1472 -- For unbound, mutable tyvars, zonkType uses the function given to it
1473 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
1474 -- type variable and zonks the kind too
1475 zonkTcType :: TcType -> TcM TcType
1476 zonkTcType = mapType zonkTcTypeMapper ()
1477
1478 -- | "Zonk" a coercion -- really, just zonk any types in the coercion
1479 zonkCo :: Coercion -> TcM Coercion
1480 zonkCo = mapCoercion zonkTcTypeMapper ()
1481
1482 zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
1483 -- A tyvar binder is never a unification variable (MetaTv),
1484 -- rather it is always a skolems. BUT it may have a kind
1485 -- that has not yet been zonked, and may include kind
1486 -- unification variables.
1487 zonkTcTyCoVarBndr tyvar
1488 -- can't use isCoVar, because it looks at a TyCon. Argh.
1489 = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), pprTyVar tyvar )
1490 updateTyVarKindM zonkTcType tyvar
1491
1492 zonkTcTyVarBinder :: TyVarBndr TcTyVar vis -> TcM (TyVarBndr TcTyVar vis)
1493 zonkTcTyVarBinder (TvBndr tv vis)
1494 = do { tv' <- zonkTcTyCoVarBndr tv
1495 ; return (TvBndr tv' vis) }
1496
1497 zonkTcTyVar :: TcTyVar -> TcM TcType
1498 -- Simply look through all Flexis
1499 zonkTcTyVar tv
1500 | isTcTyVar tv
1501 = case tcTyVarDetails tv of
1502 SkolemTv {} -> zonk_kind_and_return
1503 RuntimeUnk {} -> zonk_kind_and_return
1504 MetaTv { mtv_ref = ref }
1505 -> do { cts <- readMutVar ref
1506 ; case cts of
1507 Flexi -> zonk_kind_and_return
1508 Indirect ty -> zonkTcType ty }
1509
1510 | otherwise -- coercion variable
1511 = zonk_kind_and_return
1512 where
1513 zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv
1514 ; return (mkTyVarTy z_tv) }
1515
1516 -- Variant that assumes that any result of zonking is still a TyVar.
1517 -- Should be used only on skolems and SigTvs
1518 zonkTcTyVarToTyVar :: TcTyVar -> TcM TcTyVar
1519 zonkTcTyVarToTyVar tv
1520 = do { ty <- zonkTcTyVar tv
1521 ; return (tcGetTyVar "zonkTcTyVarToVar" ty) }
1522
1523 {-
1524 %************************************************************************
1525 %* *
1526 Tidying
1527 * *
1528 ************************************************************************
1529 -}
1530
1531 zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
1532 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
1533 ; return (tidyOpenType env ty') }
1534
1535 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
1536 zonkTidyOrigin env (GivenOrigin skol_info)
1537 = do { skol_info1 <- zonkSkolemInfo skol_info
1538 ; let skol_info2 = tidySkolemInfo env skol_info1
1539 ; return (env, GivenOrigin skol_info2) }
1540 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act
1541 , uo_expected = exp })
1542 = do { (env1, act') <- zonkTidyTcType env act
1543 ; (env2, exp') <- zonkTidyTcType env1 exp
1544 ; return ( env2, orig { uo_actual = act'
1545 , uo_expected = exp' }) }
1546 zonkTidyOrigin env (KindEqOrigin ty1 m_ty2 orig t_or_k)
1547 = do { (env1, ty1') <- zonkTidyTcType env ty1
1548 ; (env2, m_ty2') <- case m_ty2 of
1549 Just ty2 -> second Just <$> zonkTidyTcType env1 ty2
1550 Nothing -> return (env1, Nothing)
1551 ; (env3, orig') <- zonkTidyOrigin env2 orig
1552 ; return (env3, KindEqOrigin ty1' m_ty2' orig' t_or_k) }
1553 zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
1554 = do { (env1, p1') <- zonkTidyTcType env p1
1555 ; (env2, p2') <- zonkTidyTcType env1 p2
1556 ; return (env2, FunDepOrigin1 p1' l1 p2' l2) }
1557 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
1558 = do { (env1, p1') <- zonkTidyTcType env p1
1559 ; (env2, p2') <- zonkTidyTcType env1 p2
1560 ; (env3, o1') <- zonkTidyOrigin env2 o1
1561 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
1562 zonkTidyOrigin env orig = return (env, orig)
1563
1564 ----------------
1565 tidyCt :: TidyEnv -> Ct -> Ct
1566 -- Used only in error reporting
1567 -- Also converts it to non-canonical
1568 tidyCt env ct
1569 = case ct of
1570 CHoleCan { cc_ev = ev }
1571 -> ct { cc_ev = tidy_ev env ev }
1572 _ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
1573 where
1574 tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
1575 -- NB: we do not tidy the ctev_evar field because we don't
1576 -- show it in error messages
1577 tidy_ev env ctev@(CtGiven { ctev_pred = pred })
1578 = ctev { ctev_pred = tidyType env pred }
1579 tidy_ev env ctev@(CtWanted { ctev_pred = pred })
1580 = ctev { ctev_pred = tidyType env pred }
1581 tidy_ev env ctev@(CtDerived { ctev_pred = pred })
1582 = ctev { ctev_pred = tidyType env pred }
1583
1584 ----------------
1585 tidyEvVar :: TidyEnv -> EvVar -> EvVar
1586 tidyEvVar env var = setVarType var (tidyType env (varType var))
1587
1588 ----------------
1589 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
1590 tidySkolemInfo env (DerivSkol ty) = DerivSkol (tidyType env ty)
1591 tidySkolemInfo env (SigSkol cx ty tv_prs) = tidySigSkol env cx ty tv_prs
1592 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
1593 tidySkolemInfo env (UnifyForAllSkol ty) = UnifyForAllSkol (tidyType env ty)
1594 tidySkolemInfo _ info = info
1595
1596 tidySigSkol :: TidyEnv -> UserTypeCtxt
1597 -> TcType -> [(Name,TcTyVar)] -> SkolemInfo
1598 -- We need to take special care when tidying SigSkol
1599 -- See Note [SigSkol SkolemInfo] in TcRnTypes
1600 tidySigSkol env cx ty tv_prs
1601 = SigSkol cx (tidy_ty env ty) tv_prs'
1602 where
1603 tv_prs' = mapSnd (tidyTyVarOcc env) tv_prs
1604 inst_env = mkNameEnv tv_prs'
1605
1606 tidy_ty env (ForAllTy (TvBndr tv vis) ty)
1607 = ForAllTy (TvBndr tv' vis) (tidy_ty env' ty)
1608 where
1609 (env', tv') = tidy_tv_bndr env tv
1610
1611 tidy_ty env (FunTy arg res)
1612 = FunTy (tidyType env arg) (tidy_ty env res)
1613
1614 tidy_ty env ty = tidyType env ty
1615
1616 tidy_tv_bndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
1617 tidy_tv_bndr env@(occ_env, subst) tv
1618 | Just tv' <- lookupNameEnv inst_env (tyVarName tv)
1619 = ((occ_env, extendVarEnv subst tv tv'), tv')
1620
1621 | otherwise
1622 = tidyTyCoVarBndr env tv
1623
1624 -------------------------------------------------------------------------
1625 {-
1626 %************************************************************************
1627 %* *
1628 Levity polymorphism checks
1629 * *
1630 ************************************************************************
1631
1632 See Note [Levity polymorphism checking] in DsMonad
1633
1634 -}
1635
1636 -- | According to the rules around representation polymorphism
1637 -- (see https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds), no binder
1638 -- can have a representation-polymorphic type. This check ensures
1639 -- that we respect this rule. It is a bit regrettable that this error
1640 -- occurs in zonking, after which we should have reported all errors.
1641 -- But it's hard to see where else to do it, because this can be discovered
1642 -- only after all solving is done. And, perhaps most importantly, this
1643 -- isn't really a compositional property of a type system, so it's
1644 -- not a terrible surprise that the check has to go in an awkward spot.
1645 ensureNotLevPoly :: Type -- its zonked type
1646 -> SDoc -- where this happened
1647 -> TcM ()
1648 ensureNotLevPoly ty doc
1649 = whenNoErrs $ -- sometimes we end up zonking bogus definitions of type
1650 -- forall a. a. See, for example, test ghci/scripts/T9140
1651 checkForLevPoly doc ty
1652
1653 -- See Note [Levity polymorphism checking] in DsMonad
1654 checkForLevPoly :: SDoc -> Type -> TcM ()
1655 checkForLevPoly = checkForLevPolyX addErr
1656
1657 checkForLevPolyX :: Monad m
1658 => (SDoc -> m ()) -- how to report an error
1659 -> SDoc -> Type -> m ()
1660 checkForLevPolyX add_err extra ty
1661 | isTypeLevPoly ty
1662 = add_err (formatLevPolyErr ty $$ extra)
1663 | otherwise
1664 = return ()
1665
1666 formatLevPolyErr :: Type -- levity-polymorphic type
1667 -> SDoc
1668 formatLevPolyErr ty
1669 = hang (text "A levity-polymorphic type is not allowed here:")
1670 2 (vcat [ text "Type:" <+> ppr tidy_ty
1671 , text "Kind:" <+> ppr tidy_ki ])
1672 where
1673 (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty
1674 tidy_ki = tidyType tidy_env (typeKind ty)