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