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