never executed always true always false
1
2 {-# LANGUAGE MultiWayIf #-}
3 {-# LANGUAGE TupleSections #-}
4
5 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
6 {-
7 (c) The University of Glasgow 2006
8 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
9
10 -}
11
12 -- | Monadic type operations
13 --
14 -- This module contains monadic operations over types that contain mutable type
15 -- variables.
16 module GHC.Tc.Utils.TcMType (
17 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
18
19 --------------------------------
20 -- Creating new mutable type variables
21 newFlexiTyVar,
22 newNamedFlexiTyVar,
23 newFlexiTyVarTy, -- Kind -> TcM TcType
24 newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
25 newOpenFlexiTyVar, newOpenFlexiTyVarTy, newOpenTypeKind,
26 newOpenBoxedTypeKind,
27 newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel,
28 newAnonMetaTyVar, cloneMetaTyVar,
29 newCycleBreakerTyVar,
30
31 newMultiplicityVar,
32 readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
33 newTauTvDetailsAtLevel, newMetaDetails, newMetaTyVarName,
34 isFilledMetaTyVar_maybe, isFilledMetaTyVar, isUnfilledMetaTyVar,
35
36 --------------------------------
37 -- Creating new evidence variables
38 newEvVar, newEvVars, newDict,
39 newWanted, newWanteds, cloneWanted, cloneWC,
40 emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
41 emitDerivedEqs,
42 newTcEvBinds, newNoTcEvBinds, addTcEvBind,
43 emitNewExprHole,
44
45 newCoercionHole, fillCoercionHole, isFilledCoercionHole,
46 unpackCoercionHole, unpackCoercionHole_maybe,
47 checkCoercionHole,
48
49 newImplication,
50
51 --------------------------------
52 -- Instantiation
53 newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
54 newMetaTyVarTyVarX,
55 newTyVarTyVar, cloneTyVarTyVar,
56 newPatSigTyVar, newSkolemTyVar, newWildCardX,
57
58 --------------------------------
59 -- Expected types
60 ExpType(..), ExpSigmaType, ExpRhoType,
61 mkCheckExpType, newInferExpType, tcInfer,
62 readExpType, readExpType_maybe, readScaledExpType,
63 expTypeToType, scaledExpTypeToType,
64 checkingExpType_maybe, checkingExpType,
65 inferResultToType, fillInferResult, promoteTcType,
66
67 --------------------------------
68 -- Zonking and tidying
69 zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, zonkTidyOrigins,
70 tidyEvVar, tidyCt, tidyHole, tidySkolemInfo,
71 zonkTcTyVar, zonkTcTyVars,
72 zonkTcTyVarToTyVar, zonkInvisTVBinder,
73 zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkDTyCoVarSetAndFV,
74 zonkTyCoVarsAndFVList,
75
76 zonkTcType, zonkTcTypes, zonkCo,
77 zonkTyCoVarKind, zonkTyCoVarKindBinder,
78 zonkEvVar, zonkWC, zonkImplication, zonkSimples,
79 zonkId, zonkCoVar,
80 zonkCt, zonkSkolemInfo,
81
82 ---------------------------------
83 -- Promotion, defaulting, skolemisation
84 defaultTyVar, promoteMetaTyVarTo, promoteTyVarSet,
85 quantifyTyVars, isQuantifiableTv,
86 skolemiseUnboundMetaTyVar, zonkAndSkolemise, skolemiseQuantifiedTyVar,
87 doNotQuantifyTyVars,
88
89 candidateQTyVarsOfType, candidateQTyVarsOfKind,
90 candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
91 CandidatesQTvs(..), delCandidates,
92 candidateKindVars, partitionCandidates,
93
94 ------------------------------
95 -- Representation polymorphism
96 checkTypeHasFixedRuntimeRep,
97 ) where
98
99 import GHC.Prelude
100
101 import GHC.Driver.Session
102 import qualified GHC.LanguageExtensions as LangExt
103
104 import GHC.Tc.Types.Origin
105 import GHC.Tc.Utils.Monad -- TcType, amongst others
106 import GHC.Tc.Types.Constraint
107 import GHC.Tc.Types.Evidence
108 import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyType {- , unifyKind -} )
109 import GHC.Tc.Utils.TcType
110 import GHC.Tc.Errors.Types
111
112 import GHC.Core.TyCo.Rep
113 import GHC.Core.TyCo.Ppr
114 import GHC.Core.Type
115 import GHC.Core.TyCon
116 import GHC.Core.Coercion
117 import GHC.Core.Class
118 import GHC.Core.Predicate
119 import GHC.Core.InstEnv (ClsInst(is_tys))
120
121 import GHC.Types.Var
122 import GHC.Types.Id as Id
123 import GHC.Types.Name
124 import GHC.Types.Var.Set
125
126 import GHC.Builtin.Types
127 import GHC.Types.Error
128 import GHC.Types.Var.Env
129 import GHC.Types.Name.Env
130 import GHC.Types.Unique.Set
131 import GHC.Types.Basic ( TypeOrKind(..)
132 , DefaultKindVars(..), DefaultVarsOfKind(..), allVarsOfKindDefault )
133
134 import GHC.Data.FastString
135 import GHC.Data.Bag
136 import GHC.Data.Pair
137
138 import GHC.Utils.Misc
139 import GHC.Utils.Outputable
140 import GHC.Utils.Panic
141 import GHC.Utils.Panic.Plain
142 import GHC.Utils.Constants (debugIsOn)
143 import GHC.Utils.Trace
144
145 import Control.Monad
146 import GHC.Data.Maybe
147 import qualified Data.Semigroup as Semi
148
149 {-
150 ************************************************************************
151 * *
152 Kind variables
153 * *
154 ************************************************************************
155 -}
156
157 newMetaKindVar :: TcM TcKind
158 newMetaKindVar
159 = do { details <- newMetaDetails TauTv
160 ; name <- newMetaTyVarName (fsLit "k")
161 -- All MetaKindVars are called "k"
162 -- They may be jiggled by tidying
163 ; let kv = mkTcTyVar name liftedTypeKind details
164 ; traceTc "newMetaKindVar" (ppr kv)
165 ; return (mkTyVarTy kv) }
166
167 newMetaKindVars :: Int -> TcM [TcKind]
168 newMetaKindVars n = replicateM n newMetaKindVar
169
170 {-
171 ************************************************************************
172 * *
173 Evidence variables; range over constraints we can abstract over
174 * *
175 ************************************************************************
176 -}
177
178 newEvVars :: TcThetaType -> TcM [EvVar]
179 newEvVars theta = mapM newEvVar theta
180
181 --------------
182
183 newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar
184 -- Creates new *rigid* variables for predicates
185 newEvVar ty = do { name <- newSysName (predTypeOccName ty)
186 ; return (mkLocalIdOrCoVar name Many ty) }
187
188 newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
189 -- Deals with both equality and non-equality predicates
190 newWanted orig t_or_k pty
191 = do loc <- getCtLocM orig t_or_k
192 d <- if isEqPrimPred pty then HoleDest <$> newCoercionHole pty
193 else EvVarDest <$> newEvVar pty
194 return $ CtWanted { ctev_dest = d
195 , ctev_pred = pty
196 , ctev_nosh = WDeriv
197 , ctev_loc = loc }
198
199 newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
200 newWanteds orig = mapM (newWanted orig Nothing)
201
202 ----------------------------------------------
203 -- Cloning constraints
204 ----------------------------------------------
205
206 cloneWanted :: Ct -> TcM Ct
207 cloneWanted ct
208 | ev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _ }) <- ctEvidence ct
209 = do { co_hole <- newCoercionHole pty
210 ; return (mkNonCanonical (ev { ctev_dest = HoleDest co_hole })) }
211 | otherwise
212 = return ct
213
214 cloneWC :: WantedConstraints -> TcM WantedConstraints
215 -- Clone all the evidence bindings in
216 -- a) the ic_bind field of any implications
217 -- b) the CoercionHoles of any wanted constraints
218 -- so that solving the WantedConstraints will not have any visible side
219 -- effect, /except/ from causing unifications
220 cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
221 = do { simples' <- mapBagM cloneWanted simples
222 ; implics' <- mapBagM cloneImplication implics
223 ; return (wc { wc_simple = simples', wc_impl = implics' }) }
224
225 cloneImplication :: Implication -> TcM Implication
226 cloneImplication implic@(Implic { ic_binds = binds, ic_wanted = inner_wanted })
227 = do { binds' <- cloneEvBindsVar binds
228 ; inner_wanted' <- cloneWC inner_wanted
229 ; return (implic { ic_binds = binds', ic_wanted = inner_wanted' }) }
230
231 ----------------------------------------------
232 -- Emitting constraints
233 ----------------------------------------------
234
235 -- | Emits a new Wanted. Deals with both equalities and non-equalities.
236 emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
237 emitWanted origin pty
238 = do { ev <- newWanted origin Nothing pty
239 ; emitSimple $ mkNonCanonical ev
240 ; return $ ctEvTerm ev }
241
242 emitDerivedEqs :: CtOrigin -> [(TcType,TcType)] -> TcM ()
243 -- Emit some new derived nominal equalities
244 emitDerivedEqs origin pairs
245 | null pairs
246 = return ()
247 | otherwise
248 = do { loc <- getCtLocM origin Nothing
249 ; emitSimples (listToBag (map (mk_one loc) pairs)) }
250 where
251 mk_one loc (ty1, ty2)
252 = mkNonCanonical $
253 CtDerived { ctev_pred = mkPrimEqPred ty1 ty2
254 , ctev_loc = loc }
255
256 -- | Emits a new equality constraint
257 emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
258 emitWantedEq origin t_or_k role ty1 ty2
259 = do { hole <- newCoercionHole pty
260 ; loc <- getCtLocM origin (Just t_or_k)
261 ; emitSimple $ mkNonCanonical $
262 CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
263 , ctev_nosh = WDeriv, ctev_loc = loc }
264 ; return (HoleCo hole) }
265 where
266 pty = mkPrimEqPredRole role ty1 ty2
267
268 -- | Creates a new EvVar and immediately emits it as a Wanted.
269 -- No equality predicates here.
270 emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
271 emitWantedEvVar origin ty
272 = do { new_cv <- newEvVar ty
273 ; loc <- getCtLocM origin Nothing
274 ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
275 , ctev_pred = ty
276 , ctev_nosh = WDeriv
277 , ctev_loc = loc }
278 ; emitSimple $ mkNonCanonical ctev
279 ; return new_cv }
280
281 emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
282 emitWantedEvVars orig = mapM (emitWantedEvVar orig)
283
284 -- | Emit a new wanted expression hole
285 emitNewExprHole :: OccName -- of the hole
286 -> Type -> TcM HoleExprRef
287 emitNewExprHole occ ty
288 = do { u <- newUnique
289 ; ref <- newTcRef (pprPanic "unfilled unbound-variable evidence" (ppr u))
290 ; let her = HER ref ty u
291
292 ; loc <- getCtLocM (ExprHoleOrigin occ) (Just TypeLevel)
293
294 ; let hole = Hole { hole_sort = ExprHole her
295 , hole_occ = occ
296 , hole_ty = ty
297 , hole_loc = loc }
298 ; emitHole hole
299 ; return her }
300
301 newDict :: Class -> [TcType] -> TcM DictId
302 newDict cls tys
303 = do { name <- newSysName (mkDictOcc (getOccName cls))
304 ; return (mkLocalId name Many (mkClassPred cls tys)) }
305
306 predTypeOccName :: PredType -> OccName
307 predTypeOccName ty = case classifyPredType ty of
308 ClassPred cls _ -> mkDictOcc (getOccName cls)
309 EqPred {} -> mkVarOccFS (fsLit "co")
310 IrredPred {} -> mkVarOccFS (fsLit "irred")
311 ForAllPred {} -> mkVarOccFS (fsLit "df")
312 SpecialPred special_pred _ ->
313 case special_pred of
314 ConcretePrimPred -> mkVarOccFS (fsLit "concr")
315
316 -- | Create a new 'Implication' with as many sensible defaults for its fields
317 -- as possible. Note that the 'ic_tclvl', 'ic_binds', and 'ic_info' fields do
318 -- /not/ have sensible defaults, so they are initialized with lazy thunks that
319 -- will 'panic' if forced, so one should take care to initialize these fields
320 -- after creation.
321 --
322 -- This is monadic to look up the 'TcLclEnv', which is used to initialize
323 -- 'ic_env', and to set the -Winaccessible-code flag. See
324 -- Note [Avoid -Winaccessible-code when deriving] in "GHC.Tc.TyCl.Instance".
325 newImplication :: TcM Implication
326 newImplication
327 = do env <- getLclEnv
328 warn_inaccessible <- woptM Opt_WarnInaccessibleCode
329 return (implicationPrototype { ic_env = env
330 , ic_warn_inaccessible = warn_inaccessible })
331
332 {-
333 ************************************************************************
334 * *
335 Coercion holes
336 * *
337 ************************************************************************
338 -}
339
340 newCoercionHole :: TcPredType -> TcM CoercionHole
341 newCoercionHole pred_ty
342 = do { co_var <- newEvVar pred_ty
343 ; traceTc "New coercion hole:" (ppr co_var)
344 ; ref <- newMutVar Nothing
345 ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } }
346
347 -- | Put a value in a coercion hole
348 fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
349 fillCoercionHole (CoercionHole { ch_ref = ref, ch_co_var = cv }) co = do
350 when debugIsOn $ do
351 cts <- readTcRef ref
352 whenIsJust cts $ \old_co ->
353 pprPanic "Filling a filled coercion hole" (ppr cv $$ ppr co $$ ppr old_co)
354 traceTc "Filling coercion hole" (ppr cv <+> text ":=" <+> ppr co)
355 writeTcRef ref (Just co)
356
357 -- | Is a coercion hole filled in?
358 isFilledCoercionHole :: CoercionHole -> TcM Bool
359 isFilledCoercionHole (CoercionHole { ch_ref = ref }) = isJust <$> readTcRef ref
360
361 -- | Retrieve the contents of a coercion hole. Panics if the hole
362 -- is unfilled
363 unpackCoercionHole :: CoercionHole -> TcM Coercion
364 unpackCoercionHole hole
365 = do { contents <- unpackCoercionHole_maybe hole
366 ; case contents of
367 Just co -> return co
368 Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) }
369
370 -- | Retrieve the contents of a coercion hole, if it is filled
371 unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
372 unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref
373
374 -- | Check that a coercion is appropriate for filling a hole. (The hole
375 -- itself is needed only for printing.)
376 -- Always returns the checked coercion, but this return value is necessary
377 -- so that the input coercion is forced only when the output is forced.
378 checkCoercionHole :: CoVar -> Coercion -> TcM Coercion
379 checkCoercionHole cv co
380 | debugIsOn
381 = do { cv_ty <- zonkTcType (varType cv)
382 -- co is already zonked, but cv might not be
383 ; return $
384 assertPpr (ok cv_ty)
385 (text "Bad coercion hole" <+>
386 ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role
387 , ppr cv_ty ])
388 co }
389 | otherwise
390 = return co
391
392 where
393 (Pair t1 t2, role) = coercionKindRole co
394 ok cv_ty | EqPred cv_rel cv_t1 cv_t2 <- classifyPredType cv_ty
395 = t1 `eqType` cv_t1
396 && t2 `eqType` cv_t2
397 && role == eqRelRole cv_rel
398 | otherwise
399 = False
400
401 {- **********************************************************************
402 *
403 ExpType functions
404 *
405 ********************************************************************** -}
406
407 {- Note [ExpType]
408 ~~~~~~~~~~~~~~~~~
409 An ExpType is used as the "expected type" when type-checking an expression.
410 An ExpType can hold a "hole" that can be filled in by the type-checker.
411 This allows us to have one tcExpr that works in both checking mode and
412 synthesis mode (that is, bidirectional type-checking). Previously, this
413 was achieved by using ordinary unification variables, but we don't need
414 or want that generality. (For example, #11397 was caused by doing the
415 wrong thing with unification variables.) Instead, we observe that these
416 holes should
417
418 1. never be nested
419 2. never appear as the type of a variable
420 3. be used linearly (never be duplicated)
421
422 By defining ExpType, separately from Type, we can achieve goals 1 and 2
423 statically.
424
425 See also [wiki:typechecking]
426
427 Note [TcLevel of ExpType]
428 ~~~~~~~~~~~~~~~~~~~~~~~~~
429 Consider
430
431 data G a where
432 MkG :: G Bool
433
434 foo MkG = True
435
436 This is a classic untouchable-variable / ambiguous GADT return type
437 scenario. But, with ExpTypes, we'll be inferring the type of the RHS.
438 We thus must track a TcLevel in an Inferring ExpType. If we try to
439 fill the ExpType and find that the TcLevels don't work out, we fill
440 the ExpType with a tau-tv at the low TcLevel, hopefully to be worked
441 out later by some means -- see fillInferResult, and Note [fillInferResult]
442
443 This behaviour triggered in test gadt/gadt-escape1.
444 -}
445
446 -- actual data definition is in GHC.Tc.Utils.TcType
447
448 newInferExpType :: TcM ExpType
449 newInferExpType
450 = do { u <- newUnique
451 ; tclvl <- getTcLevel
452 ; traceTc "newInferExpType" (ppr u <+> ppr tclvl)
453 ; ref <- newMutVar Nothing
454 ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl
455 , ir_ref = ref })) }
456
457 -- | Extract a type out of an ExpType, if one exists. But one should always
458 -- exist. Unless you're quite sure you know what you're doing.
459 readExpType_maybe :: ExpType -> TcM (Maybe TcType)
460 readExpType_maybe (Check ty) = return (Just ty)
461 readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
462
463 -- | Same as readExpType, but for Scaled ExpTypes
464 readScaledExpType :: Scaled ExpType -> TcM (Scaled Type)
465 readScaledExpType (Scaled m exp_ty)
466 = do { ty <- readExpType exp_ty
467 ; return (Scaled m ty) }
468
469 -- | Extract a type out of an ExpType. Otherwise, panics.
470 readExpType :: ExpType -> TcM TcType
471 readExpType exp_ty
472 = do { mb_ty <- readExpType_maybe exp_ty
473 ; case mb_ty of
474 Just ty -> return ty
475 Nothing -> pprPanic "Unknown expected type" (ppr exp_ty) }
476
477 -- | Returns the expected type when in checking mode.
478 checkingExpType_maybe :: ExpType -> Maybe TcType
479 checkingExpType_maybe (Check ty) = Just ty
480 checkingExpType_maybe (Infer {}) = Nothing
481
482 -- | Returns the expected type when in checking mode. Panics if in inference
483 -- mode.
484 checkingExpType :: String -> ExpType -> TcType
485 checkingExpType _ (Check ty) = ty
486 checkingExpType err et = pprPanic "checkingExpType" (text err $$ ppr et)
487
488 scaledExpTypeToType :: Scaled ExpType -> TcM (Scaled TcType)
489 scaledExpTypeToType (Scaled m exp_ty)
490 = do { ty <- expTypeToType exp_ty
491 ; return (Scaled m ty) }
492
493 -- | Extracts the expected type if there is one, or generates a new
494 -- TauTv if there isn't.
495 expTypeToType :: ExpType -> TcM TcType
496 expTypeToType (Check ty) = return ty
497 expTypeToType (Infer inf_res) = inferResultToType inf_res
498
499 inferResultToType :: InferResult -> TcM Type
500 inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
501 , ir_ref = ref })
502 = do { mb_inferred_ty <- readTcRef ref
503 ; tau <- case mb_inferred_ty of
504 Just ty -> do { ensureMonoType ty
505 -- See Note [inferResultToType]
506 ; return ty }
507 Nothing -> do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
508 ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
509 -- See Note [TcLevel of ExpType]
510 ; writeMutVar ref (Just tau)
511 ; return tau }
512 ; traceTc "Forcing ExpType to be monomorphic:"
513 (ppr u <+> text ":=" <+> ppr tau)
514 ; return tau }
515
516 {- Note [inferResultToType]
517 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
518 expTypeToType and inferResultType convert an InferResult to a monotype.
519 It must be a monotype because if the InferResult isn't already filled in,
520 we fill it in with a unification variable (hence monotype). So to preserve
521 order-independence we check for mono-type-ness even if it *is* filled in
522 already.
523
524 See also Note [TcLevel of ExpType] above, and
525 Note [fillInferResult].
526 -}
527
528 -- | Infer a type using a fresh ExpType
529 -- See also Note [ExpType] in "GHC.Tc.Utils.TcMType"
530 tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
531 tcInfer tc_check
532 = do { res_ty <- newInferExpType
533 ; result <- tc_check res_ty
534 ; res_ty <- readExpType res_ty
535 ; return (result, res_ty) }
536
537 fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
538 -- If co = fillInferResult t1 t2
539 -- => co :: t1 ~ t2
540 -- See Note [fillInferResult]
541 fillInferResult act_res_ty (IR { ir_uniq = u, ir_lvl = res_lvl
542 , ir_ref = ref })
543 = do { mb_exp_res_ty <- readTcRef ref
544 ; case mb_exp_res_ty of
545 Just exp_res_ty
546 -> do { traceTc "Joining inferred ExpType" $
547 ppr u <> colon <+> ppr act_res_ty <+> char '~' <+> ppr exp_res_ty
548 ; cur_lvl <- getTcLevel
549 ; unless (cur_lvl `sameDepthAs` res_lvl) $
550 ensureMonoType act_res_ty
551 ; unifyType Nothing act_res_ty exp_res_ty }
552 Nothing
553 -> do { traceTc "Filling inferred ExpType" $
554 ppr u <+> text ":=" <+> ppr act_res_ty
555 ; (prom_co, act_res_ty) <- promoteTcType res_lvl act_res_ty
556 ; writeTcRef ref (Just act_res_ty)
557 ; return prom_co }
558 }
559
560
561 {- Note [fillInferResult]
562 ~~~~~~~~~~~~~~~~~~~~~~~~~
563 When inferring, we use fillInferResult to "fill in" the hole in InferResult
564 data InferResult = IR { ir_uniq :: Unique
565 , ir_lvl :: TcLevel
566 , ir_ref :: IORef (Maybe TcType) }
567
568 There are two things to worry about:
569
570 1. What if it is under a GADT or existential pattern match?
571 - GADTs: a unification variable (and Infer's hole is similar) is untouchable
572 - Existentials: be careful about skolem-escape
573
574 2. What if it is filled in more than once? E.g. multiple branches of a case
575 case e of
576 T1 -> e1
577 T2 -> e2
578
579 Our typing rules are:
580
581 * The RHS of a existential or GADT alternative must always be a
582 monotype, regardless of the number of alternatives.
583
584 * Multiple non-existential/GADT branches can have (the same)
585 higher rank type (#18412). E.g. this is OK:
586 case e of
587 True -> hr
588 False -> hr
589 where hr:: (forall a. a->a) -> Int
590 c.f. Section 7.1 of "Practical type inference for arbitrary-rank types"
591 We use choice (2) in that Section.
592 (GHC 8.10 and earlier used choice (1).)
593
594 But note that
595 case e of
596 True -> hr
597 False -> \x -> hr x
598 will fail, because we still /infer/ both branches, so the \x will get
599 a (monotype) unification variable, which will fail to unify with
600 (forall a. a->a)
601
602 For (1) we can detect the GADT/existential situation by seeing that
603 the current TcLevel is greater than that stored in ir_lvl of the Infer
604 ExpType. We bump the level whenever we go past a GADT/existential match.
605
606 Then, before filling the hole use promoteTcType to promote the type
607 to the outer ir_lvl. promoteTcType does this
608 - create a fresh unification variable alpha at level ir_lvl
609 - emits an equality alpha[ir_lvl] ~ ty
610 - fills the hole with alpha
611 That forces the type to be a monotype (since unification variables can
612 only unify with monotypes); and catches skolem-escapes because the
613 alpha is untouchable until the equality floats out.
614
615 For (2), we simply look to see if the hole is filled already.
616 - if not, we promote (as above) and fill the hole
617 - if it is filled, we simply unify with the type that is
618 already there
619
620 There is one wrinkle. Suppose we have
621 case e of
622 T1 -> e1 :: (forall a. a->a) -> Int
623 G2 -> e2
624 where T1 is not GADT or existential, but G2 is a GADT. Then supppose the
625 T1 alternative fills the hole with (forall a. a->a) -> Int, which is fine.
626 But now the G2 alternative must not *just* unify with that else we'd risk
627 allowing through (e2 :: (forall a. a->a) -> Int). If we'd checked G2 first
628 we'd have filled the hole with a unification variable, which enforces a
629 monotype.
630
631 So if we check G2 second, we still want to emit a constraint that restricts
632 the RHS to be a monotype. This is done by ensureMonoType, and it works
633 by simply generating a constraint (alpha ~ ty), where alpha is a fresh
634 unification variable. We discard the evidence.
635
636 -}
637
638 {- *********************************************************************
639 * *
640 Promoting types
641 * *
642 ********************************************************************* -}
643
644 ensureMonoType :: TcType -> TcM ()
645 -- Assuming that the argument type is of kind (TYPE r),
646 -- ensure that it is a /monotype/
647 -- If it is not a monotype we can see right away (since unification
648 -- varibles and type-function applications stand for monotypes), but
649 -- we emit a Wanted equality just to delay the error message until later
650 ensureMonoType res_ty
651 | isTauTy res_ty -- isTauTy doesn't need zonking or anything
652 = return ()
653 | otherwise
654 = do { mono_ty <- newOpenFlexiTyVarTy
655 ; let eq_orig = TypeEqOrigin { uo_actual = res_ty
656 , uo_expected = mono_ty
657 , uo_thing = Nothing
658 , uo_visible = False }
659
660 ; _co <- emitWantedEq eq_orig TypeLevel Nominal res_ty mono_ty
661 ; return () }
662
663 promoteTcType :: TcLevel -> TcType -> TcM (TcCoercionN, TcType)
664 -- See Note [Promoting a type]
665 -- See also Note [fillInferResult]
666 -- promoteTcType level ty = (co, ty')
667 -- * Returns ty' whose max level is just 'level'
668 -- and whose kind is ~# to the kind of 'ty'
669 -- and whose kind has form TYPE rr
670 -- * and co :: ty ~ ty'
671 -- * and emits constraints to justify the coercion
672 --
673 -- NB: we expect that 'ty' has already kind (TYPE rr) for
674 -- some rr::RuntimeRep. It is, after all, the type of a term.
675 promoteTcType dest_lvl ty
676 = do { cur_lvl <- getTcLevel
677 ; if (cur_lvl `sameDepthAs` dest_lvl)
678 then return (mkTcNomReflCo ty, ty)
679 else promote_it }
680 where
681 promote_it :: TcM (TcCoercion, TcType)
682 promote_it -- Emit a constraint (alpha :: TYPE rr) ~ ty
683 -- where alpha and rr are fresh and from level dest_lvl
684 = do { rr <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy
685 ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (tYPE rr)
686 ; let eq_orig = TypeEqOrigin { uo_actual = ty
687 , uo_expected = prom_ty
688 , uo_thing = Nothing
689 , uo_visible = False }
690
691 ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty
692 ; return (co, prom_ty) }
693
694 {- Note [Promoting a type]
695 ~~~~~~~~~~~~~~~~~~~~~~~~~~
696 Consider (#12427)
697
698 data T where
699 MkT :: (Int -> Int) -> a -> T
700
701 h y = case y of MkT v w -> v
702
703 We'll infer the RHS type with an expected type ExpType of
704 (IR { ir_lvl = l, ir_ref = ref, ... )
705 where 'l' is the TcLevel of the RHS of 'h'. Then the MkT pattern
706 match will increase the level, so we'll end up in tcSubType, trying to
707 unify the type of v,
708 v :: Int -> Int
709 with the expected type. But this attempt takes place at level (l+1),
710 rightly so, since v's type could have mentioned existential variables,
711 (like w's does) and we want to catch that.
712
713 So we
714 - create a new meta-var alpha[l+1]
715 - fill in the InferRes ref cell 'ref' with alpha
716 - emit an equality constraint, thus
717 [W] alpha[l+1] ~ (Int -> Int)
718
719 That constraint will float outwards, as it should, unless v's
720 type mentions a skolem-captured variable.
721
722 This approach fails if v has a higher rank type; see
723 Note [Promotion and higher rank types]
724
725
726 Note [Promotion and higher rank types]
727 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
728 If v had a higher-rank type, say v :: (forall a. a->a) -> Int,
729 then we'd emit an equality
730 [W] alpha[l+1] ~ ((forall a. a->a) -> Int)
731 which will sadly fail because we can't unify a unification variable
732 with a polytype. But there is nothing really wrong with the program
733 here.
734
735 We could just about solve this by "promote the type" of v, to expose
736 its polymorphic "shape" while still leaving constraints that will
737 prevent existential escape. But we must be careful! Exposing
738 the "shape" of the type is precisely what we must NOT do under
739 a GADT pattern match! So in this case we might promote the type
740 to
741 (forall a. a->a) -> alpha[l+1]
742 and emit the constraint
743 [W] alpha[l+1] ~ Int
744 Now the promoted type can fill the ref cell, while the emitted
745 equality can float or not, according to the usual rules.
746
747 But that's not quite right! We are exposing the arrow! We could
748 deal with that too:
749 (forall a. mu[l+1] a a) -> alpha[l+1]
750 with constraints
751 [W] alpha[l+1] ~ Int
752 [W] mu[l+1] ~ (->)
753 Here we abstract over the '->' inside the forall, in case that
754 is subject to an equality constraint from a GADT match.
755
756 Note that we kept the outer (->) because that's part of
757 the polymorphic "shape". And because of impredicativity,
758 GADT matches can't give equalities that affect polymorphic
759 shape.
760
761 This reasoning just seems too complicated, so I decided not
762 to do it. These higher-rank notes are just here to record
763 the thinking.
764 -}
765
766
767 {- *********************************************************************
768 * *
769 MetaTvs (meta type variables; mutable)
770 * *
771 ********************************************************************* -}
772
773 {- Note [TyVarTv]
774 ~~~~~~~~~~~~~~~~~
775 A TyVarTv can unify with type *variables* only, including other TyVarTvs and
776 skolems. They are used in two places:
777
778 1. In kind signatures, see GHC.Tc.TyCl
779 Note [Inferring kinds for type declarations]
780 and Note [Kind checking for GADTs]
781
782 2. In partial type signatures. See GHC.Tc.Types
783 Note [Quantified variables in partial type signatures]
784
785 Sometimes, they can unify with type variables that the user would
786 rather keep distinct; see #11203 for an example. So, any client of
787 this function needs to either allow the TyVarTvs to unify with each
788 other or check that they don't. In the case of (1) the check is done
789 in GHC.Tc.TyCl.swizzleTcTyConBndrs. In case of (2) it's done by
790 findDupTyVarTvs in GHC.Tc.Gen.Bind.chooseInferredQuantifiers.
791
792 Historical note: Before #15050 this (under the name SigTv) was also
793 used for ScopedTypeVariables in patterns, to make sure these type
794 variables only refer to other type variables, but this restriction was
795 dropped, and ScopedTypeVariables can now refer to full types (GHC
796 Proposal 29).
797 -}
798
799 newMetaTyVarName :: FastString -> TcM Name
800 -- Makes a /System/ Name, which is eagerly eliminated by
801 -- the unifier; see GHC.Tc.Utils.Unify.nicer_to_update_tv1, and
802 -- GHC.Tc.Solver.Canonical.canEqTyVarTyVar (nicer_to_update_tv2)
803 newMetaTyVarName str
804 = do { uniq <- newUnique
805 ; return (mkSystemName uniq (mkTyVarOccFS str)) }
806
807 cloneMetaTyVarName :: Name -> TcM Name
808 cloneMetaTyVarName name
809 = do { uniq <- newUnique
810 ; return (mkSystemName uniq (nameOccName name)) }
811 -- See Note [Name of an instantiated type variable]
812
813 {- Note [Name of an instantiated type variable]
814 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
815 At the moment we give a unification variable a System Name, which
816 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
817 -}
818
819 metaInfoToTyVarName :: MetaInfo -> FastString
820 metaInfoToTyVarName meta_info =
821 case meta_info of
822 TauTv -> fsLit "t"
823 TyVarTv -> fsLit "a"
824 RuntimeUnkTv -> fsLit "r"
825 CycleBreakerTv -> fsLit "b"
826
827 newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
828 newAnonMetaTyVar mi = newNamedAnonMetaTyVar (metaInfoToTyVarName mi) mi
829
830 newNamedAnonMetaTyVar :: FastString -> MetaInfo -> Kind -> TcM TcTyVar
831 -- Make a new meta tyvar out of thin air
832 newNamedAnonMetaTyVar tyvar_name meta_info kind
833
834 = do { name <- newMetaTyVarName tyvar_name
835 ; details <- newMetaDetails meta_info
836 ; let tyvar = mkTcTyVar name kind details
837 ; traceTc "newAnonMetaTyVar" (ppr tyvar)
838 ; return tyvar }
839
840 -- makes a new skolem tv
841 newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
842 newSkolemTyVar name kind
843 = do { lvl <- getTcLevel
844 ; return (mkTcTyVar name kind (SkolemTv lvl False)) }
845
846 newTyVarTyVar :: Name -> Kind -> TcM TcTyVar
847 -- See Note [TyVarTv]
848 -- Does not clone a fresh unique
849 newTyVarTyVar name kind
850 = do { details <- newMetaDetails TyVarTv
851 ; let tyvar = mkTcTyVar name kind details
852 ; traceTc "newTyVarTyVar" (ppr tyvar)
853 ; return tyvar }
854
855 cloneTyVarTyVar :: Name -> Kind -> TcM TcTyVar
856 -- See Note [TyVarTv]
857 -- Clones a fresh unique
858 cloneTyVarTyVar name kind
859 = do { details <- newMetaDetails TyVarTv
860 ; uniq <- newUnique
861 ; let name' = name `setNameUnique` uniq
862 tyvar = mkTcTyVar name' kind details
863 -- Don't use cloneMetaTyVar, which makes a SystemName
864 -- We want to keep the original more user-friendly Name
865 -- In practical terms that means that in error messages,
866 -- when the Name is tidied we get 'a' rather than 'a0'
867 ; traceTc "cloneTyVarTyVar" (ppr tyvar)
868 ; return tyvar }
869
870 newPatSigTyVar :: Name -> Kind -> TcM TcTyVar
871 newPatSigTyVar name kind
872 = do { details <- newMetaDetails TauTv
873 ; uniq <- newUnique
874 ; let name' = name `setNameUnique` uniq
875 tyvar = mkTcTyVar name' kind details
876 -- Don't use cloneMetaTyVar;
877 -- same reasoning as in newTyVarTyVar
878 ; traceTc "newPatSigTyVar" (ppr tyvar)
879 ; return tyvar }
880
881 cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
882 -- Make a fresh MetaTyVar, basing the name
883 -- on that of the supplied TyVar
884 cloneAnonMetaTyVar info tv kind
885 = do { details <- newMetaDetails info
886 ; name <- cloneMetaTyVarName (tyVarName tv)
887 ; let tyvar = mkTcTyVar name kind details
888 ; traceTc "cloneAnonMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar))
889 ; return tyvar }
890
891 -- Make a new CycleBreakerTv. See Note [Type variable cycles]
892 -- in GHC.Tc.Solver.Canonical.
893 newCycleBreakerTyVar :: TcKind -> TcM TcTyVar
894 newCycleBreakerTyVar kind
895 = do { details <- newMetaDetails CycleBreakerTv
896 ; name <- newMetaTyVarName (fsLit "cbv")
897 ; return (mkTcTyVar name kind details) }
898
899 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
900 newMetaDetails info
901 = do { ref <- newMutVar Flexi
902 ; tclvl <- getTcLevel
903 ; return (MetaTv { mtv_info = info
904 , mtv_ref = ref
905 , mtv_tclvl = tclvl }) }
906
907 newTauTvDetailsAtLevel :: TcLevel -> TcM TcTyVarDetails
908 newTauTvDetailsAtLevel tclvl
909 = do { ref <- newMutVar Flexi
910 ; return (MetaTv { mtv_info = TauTv
911 , mtv_ref = ref
912 , mtv_tclvl = tclvl }) }
913
914 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
915 cloneMetaTyVar tv
916 = assert (isTcTyVar tv) $
917 do { ref <- newMutVar Flexi
918 ; name' <- cloneMetaTyVarName (tyVarName tv)
919 ; let details' = case tcTyVarDetails tv of
920 details@(MetaTv {}) -> details { mtv_ref = ref }
921 _ -> pprPanic "cloneMetaTyVar" (ppr tv)
922 tyvar = mkTcTyVar name' (tyVarKind tv) details'
923 ; traceTc "cloneMetaTyVar" (ppr tyvar)
924 ; return tyvar }
925
926 -- Works for both type and kind variables
927 readMetaTyVar :: TyVar -> TcM MetaDetails
928 readMetaTyVar tyvar = assertPpr (isMetaTyVar tyvar) (ppr tyvar) $
929 readMutVar (metaTyVarRef tyvar)
930
931 isFilledMetaTyVar_maybe :: TcTyVar -> TcM (Maybe Type)
932 isFilledMetaTyVar_maybe tv
933 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
934 = do { cts <- readTcRef ref
935 ; case cts of
936 Indirect ty -> return (Just ty)
937 Flexi -> return Nothing }
938 | otherwise
939 = return Nothing
940
941 isFilledMetaTyVar :: TyVar -> TcM Bool
942 -- True of a filled-in (Indirect) meta type variable
943 isFilledMetaTyVar tv = isJust <$> isFilledMetaTyVar_maybe tv
944
945 isUnfilledMetaTyVar :: TyVar -> TcM Bool
946 -- True of a un-filled-in (Flexi) meta type variable
947 -- NB: Not the opposite of isFilledMetaTyVar
948 isUnfilledMetaTyVar tv
949 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
950 = do { details <- readMutVar ref
951 ; return (isFlexi details) }
952 | otherwise = return False
953
954 --------------------
955 -- Works with both type and kind variables
956 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
957 -- Write into a currently-empty MetaTyVar
958
959 writeMetaTyVar tyvar ty
960 | not debugIsOn
961 = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty
962
963 -- Everything from here on only happens if DEBUG is on
964 | not (isTcTyVar tyvar)
965 = massertPpr False (text "Writing to non-tc tyvar" <+> ppr tyvar)
966
967 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
968 = writeMetaTyVarRef tyvar ref ty
969
970 | otherwise
971 = massertPpr False (text "Writing to non-meta tyvar" <+> ppr tyvar)
972
973 --------------------
974 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
975 -- Here the tyvar is for error checking only;
976 -- the ref cell must be for the same tyvar
977 writeMetaTyVarRef tyvar ref ty
978 | not debugIsOn
979 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
980 <+> text ":=" <+> ppr ty)
981 ; writeTcRef ref (Indirect ty) }
982
983 -- Everything from here on only happens if DEBUG is on
984 -- Need to zonk 'ty' because we may only recently have promoted
985 -- its free meta-tyvars (see Solver.Interact.tryToSolveByUnification)
986 | otherwise
987 = do { meta_details <- readMutVar ref;
988 -- Zonk kinds to allow the error check to work
989 ; zonked_tv_kind <- zonkTcType tv_kind
990 ; zonked_ty <- zonkTcType ty
991 ; let zonked_ty_kind = tcTypeKind zonked_ty
992 zonked_ty_lvl = tcTypeLevel zonked_ty
993 level_check_ok = not (zonked_ty_lvl `strictlyDeeperThan` tv_lvl)
994 level_check_msg = ppr zonked_ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
995 kind_check_ok = zonked_ty_kind `eqType` zonked_tv_kind
996 -- Hack alert! eqType, not tcEqType. see:
997 -- Note [coreView vs tcView] in GHC.Core.Type
998 -- Note [Extra-constraint holes in partial type signatures] in GHC.Tc.Gen.HsType
999
1000 kind_msg = hang (text "Ill-kinded update to meta tyvar")
1001 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
1002 <+> text ":="
1003 <+> ppr ty <+> text "::" <+> (ppr zonked_ty_kind) )
1004
1005 ; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
1006
1007 -- Check for double updates
1008 ; massertPpr (isFlexi meta_details) (double_upd_msg meta_details)
1009
1010 -- Check for level OK
1011 ; massertPpr level_check_ok level_check_msg
1012
1013 -- Check Kinds ok
1014 ; massertPpr kind_check_ok kind_msg
1015
1016 -- Do the write
1017 ; writeMutVar ref (Indirect ty) }
1018 where
1019 tv_kind = tyVarKind tyvar
1020
1021 tv_lvl = tcTyVarLevel tyvar
1022
1023
1024 double_upd_msg details = hang (text "Double update of meta tyvar")
1025 2 (ppr tyvar $$ ppr details)
1026
1027 {-
1028 ************************************************************************
1029 * *
1030 MetaTvs: TauTvs
1031 * *
1032 ************************************************************************
1033
1034 Note [Never need to instantiate coercion variables]
1035 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1036 With coercion variables sloshing around in types, it might seem that we
1037 sometimes need to instantiate coercion variables. This would be problematic,
1038 because coercion variables inhabit unboxed equality (~#), and the constraint
1039 solver thinks in terms only of boxed equality (~). The solution is that
1040 we never need to instantiate coercion variables in the first place.
1041
1042 The tyvars that we need to instantiate come from the types of functions,
1043 data constructors, and patterns. These will never be quantified over
1044 coercion variables, except for the special case of the promoted Eq#. But,
1045 that can't ever appear in user code, so we're safe!
1046 -}
1047
1048
1049 newMultiplicityVar :: TcM TcType
1050 newMultiplicityVar = newFlexiTyVarTy multiplicityTy
1051
1052 newFlexiTyVar :: Kind -> TcM TcTyVar
1053 newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
1054
1055 -- | Create a new flexi ty var with a specific name
1056 newNamedFlexiTyVar :: FastString -> Kind -> TcM TcTyVar
1057 newNamedFlexiTyVar fs kind = newNamedAnonMetaTyVar fs TauTv kind
1058
1059 newFlexiTyVarTy :: Kind -> TcM TcType
1060 newFlexiTyVarTy kind = do
1061 tc_tyvar <- newFlexiTyVar kind
1062 return (mkTyVarTy tc_tyvar)
1063
1064 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
1065 newFlexiTyVarTys n kind = replicateM n (newFlexiTyVarTy kind)
1066
1067 newOpenTypeKind :: TcM TcKind
1068 newOpenTypeKind
1069 = do { rr <- newFlexiTyVarTy runtimeRepTy
1070 ; return (tYPE rr) }
1071
1072 -- | Create a tyvar that can be a lifted or unlifted type.
1073 -- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh
1074 newOpenFlexiTyVarTy :: TcM TcType
1075 newOpenFlexiTyVarTy
1076 = do { tv <- newOpenFlexiTyVar
1077 ; return (mkTyVarTy tv) }
1078
1079 newOpenFlexiTyVar :: TcM TcTyVar
1080 newOpenFlexiTyVar
1081 = do { kind <- newOpenTypeKind
1082 ; newFlexiTyVar kind }
1083
1084 newOpenBoxedTypeKind :: TcM TcKind
1085 newOpenBoxedTypeKind
1086 = do { lev <- newFlexiTyVarTy (mkTyConTy levityTyCon)
1087 ; let rr = mkTyConApp boxedRepDataConTyCon [lev]
1088 ; return (tYPE rr) }
1089
1090 newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
1091 -- Instantiate with META type variables
1092 -- Note that this works for a sequence of kind, type, and coercion variables
1093 -- variables. Eg [ (k:*), (a:k->k) ]
1094 -- Gives [ (k7:*), (a8:k7->k7) ]
1095 newMetaTyVars = newMetaTyVarsX emptyTCvSubst
1096 -- emptyTCvSubst has an empty in-scope set, but that's fine here
1097 -- Since the tyvars are freshly made, they cannot possibly be
1098 -- captured by any existing for-alls.
1099
1100 newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
1101 -- Just like newMetaTyVars, but start with an existing substitution.
1102 newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
1103
1104 newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
1105 -- Make a new unification variable tyvar whose Name and Kind come from
1106 -- an existing TyVar. We substitute kind variables in the kind.
1107 newMetaTyVarX = new_meta_tv_x TauTv
1108
1109 newMetaTyVarTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
1110 -- Just like newMetaTyVarX, but make a TyVarTv
1111 newMetaTyVarTyVarX = new_meta_tv_x TyVarTv
1112
1113 newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
1114 newWildCardX subst tv
1115 = do { new_tv <- newAnonMetaTyVar TauTv (substTy subst (tyVarKind tv))
1116 ; return (extendTvSubstWithClone subst tv new_tv, new_tv) }
1117
1118 new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
1119 new_meta_tv_x info subst tv
1120 = do { new_tv <- cloneAnonMetaTyVar info tv substd_kind
1121 ; let subst1 = extendTvSubstWithClone subst tv new_tv
1122 ; return (subst1, new_tv) }
1123 where
1124 substd_kind = substTyUnchecked subst (tyVarKind tv)
1125 -- NOTE: #12549 is fixed so we could use
1126 -- substTy here, but the tc_infer_args problem
1127 -- is not yet fixed so leaving as unchecked for now.
1128 -- OLD NOTE:
1129 -- Unchecked because we call newMetaTyVarX from
1130 -- tcInstTyBinder, which is called from tcInferTyApps
1131 -- which does not yet take enough trouble to ensure
1132 -- the in-scope set is right; e.g. #12785 trips
1133 -- if we use substTy here
1134
1135 newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
1136 newMetaTyVarTyAtLevel tc_lvl kind
1137 = do { details <- newTauTvDetailsAtLevel tc_lvl
1138 ; name <- newMetaTyVarName (fsLit "p")
1139 ; return (mkTyVarTy (mkTcTyVar name kind details)) }
1140
1141 {- *********************************************************************
1142 * *
1143 Finding variables to quantify over
1144 * *
1145 ********************************************************************* -}
1146
1147 {- Note [Dependent type variables]
1148 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1149 In Haskell type inference we quantify over type variables; but we only
1150 quantify over /kind/ variables when -XPolyKinds is on. Without -XPolyKinds
1151 we default the kind variables to *.
1152
1153 So, to support this defaulting, and only for that reason, when
1154 collecting the free vars of a type (in candidateQTyVarsOfType and friends),
1155 prior to quantifying, we must keep the type and kind variables separate.
1156
1157 But what does that mean in a system where kind variables /are/ type
1158 variables? It's a fairly arbitrary distinction based on how the
1159 variables appear:
1160
1161 - "Kind variables" appear in the kind of some other free variable
1162 or in the kind of a locally quantified type variable
1163 (forall (a :: kappa). ...) or in the kind of a coercion
1164 (a |> (co :: kappa1 ~ kappa2)).
1165
1166 These are the ones we default to * if -XPolyKinds is off
1167
1168 - "Type variables" are all free vars that are not kind variables
1169
1170 E.g. In the type T k (a::k)
1171 'k' is a kind variable, because it occurs in the kind of 'a',
1172 even though it also appears at "top level" of the type
1173 'a' is a type variable, because it doesn't
1174
1175 We gather these variables using a CandidatesQTvs record:
1176 DV { dv_kvs: Variables free in the kind of a free type variable
1177 or of a forall-bound type variable
1178 , dv_tvs: Variables syntactically free in the type }
1179
1180 So: dv_kvs are the kind variables of the type
1181 (dv_tvs - dv_kvs) are the type variable of the type
1182
1183 Note that
1184
1185 * A variable can occur in both.
1186 T k (x::k) The first occurrence of k makes it
1187 show up in dv_tvs, the second in dv_kvs
1188
1189 * We include any coercion variables in the "dependent",
1190 "kind-variable" set because we never quantify over them.
1191
1192 * The "kind variables" might depend on each other; e.g
1193 (k1 :: k2), (k2 :: *)
1194 The "type variables" do not depend on each other; if
1195 one did, it'd be classified as a kind variable!
1196
1197 Note [CandidatesQTvs determinism and order]
1198 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1199 * Determinism: when we quantify over type variables we decide the
1200 order in which they appear in the final type. Because the order of
1201 type variables in the type can end up in the interface file and
1202 affects some optimizations like worker-wrapper, we want this order to
1203 be deterministic.
1204
1205 To achieve that we use deterministic sets of variables that can be
1206 converted to lists in a deterministic order. For more information
1207 about deterministic sets see Note [Deterministic UniqFM] in GHC.Types.Unique.DFM.
1208
1209 * Order: as well as being deterministic, we use an
1210 accumulating-parameter style for candidateQTyVarsOfType so that we
1211 add variables one at a time, left to right. That means we tend to
1212 produce the variables in left-to-right order. This is just to make
1213 it bit more predictable for the programmer.
1214
1215 Note [Naughty quantification candidates]
1216 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1217 Consider (#14880, dependent/should_compile/T14880-2), suppose
1218 we are trying to generalise this type:
1219
1220 forall arg. ... (alpha[tau]:arg) ...
1221
1222 We have a metavariable alpha whose kind mentions a skolem variable
1223 bound inside the very type we are generalising.
1224 This can arise while type-checking a user-written type signature
1225 (see the test case for the full code).
1226
1227 We cannot generalise over alpha! That would produce a type like
1228 forall {a :: arg}. forall arg. ...blah...
1229 The fact that alpha's kind mentions arg renders it completely
1230 ineligible for generalisation.
1231
1232 However, we are not going to learn any new constraints on alpha,
1233 because its kind isn't even in scope in the outer context (but see Wrinkle).
1234 So alpha is entirely unconstrained.
1235
1236 What then should we do with alpha? During generalization, every
1237 metavariable is either (A) promoted, (B) generalized, or (C) zapped
1238 (according to Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType).
1239
1240 * We can't generalise it.
1241 * We can't promote it, because its kind prevents that
1242 * We can't simply leave it be, because this type is about to
1243 go into the typing environment (as the type of some let-bound
1244 variable, say), and then chaos erupts when we try to instantiate.
1245
1246 Previously, we zapped it to Any. This worked, but it had the unfortunate
1247 effect of causing Any sometimes to appear in error messages. If this
1248 kind of signature happens, the user probably has made a mistake -- no
1249 one really wants Any in their types. So we now error. This must be
1250 a hard error (failure in the monad) to avoid other messages from mentioning
1251 Any.
1252
1253 We do this eager erroring in candidateQTyVars, which always precedes
1254 generalisation, because at that moment we have a clear picture of what
1255 skolems are in scope within the type itself (e.g. that 'forall arg').
1256
1257 This change is inspired by and described in Section 7.2 of "Kind Inference
1258 for Datatypes", POPL'20.
1259
1260 NB: this is all rather similar to, but sadly not the same as
1261 Note [Error on unconstrained meta-variables]
1262
1263 Wrinkle:
1264
1265 We must make absolutely sure that alpha indeed is not
1266 from an outer context. (Otherwise, we might indeed learn more information
1267 about it.) This can be done easily: we just check alpha's TcLevel.
1268 That level must be strictly greater than the ambient TcLevel in order
1269 to treat it as naughty. We say "strictly greater than" because the call to
1270 candidateQTyVars is made outside the bumped TcLevel, as stated in the
1271 comment to candidateQTyVarsOfType. The level check is done in go_tv
1272 in collect_cand_qtvs. Skipping this check caused #16517.
1273
1274 -}
1275
1276 data CandidatesQTvs
1277 -- See Note [Dependent type variables]
1278 -- See Note [CandidatesQTvs determinism and order]
1279 --
1280 -- Invariants:
1281 -- * All variables are fully zonked, including their kinds
1282 -- * All variables are at a level greater than the ambient level
1283 -- See Note [Use level numbers for quantification]
1284 --
1285 -- This *can* contain skolems. For example, in `data X k :: k -> Type`
1286 -- we need to know that the k is a dependent variable. This is done
1287 -- by collecting the candidates in the kind after skolemising. It also
1288 -- comes up when generalizing a associated type instance, where instance
1289 -- variables are skolems. (Recall that associated type instances are generalized
1290 -- independently from their enclosing class instance, and the associated
1291 -- type instance may be generalized by more, fewer, or different variables
1292 -- than the class instance.)
1293 --
1294 = DV { dv_kvs :: DTyVarSet -- "kind" metavariables (dependent)
1295 , dv_tvs :: DTyVarSet -- "type" metavariables (non-dependent)
1296 -- A variable may appear in both sets
1297 -- E.g. T k (x::k) The first occurrence of k makes it
1298 -- show up in dv_tvs, the second in dv_kvs
1299 -- See Note [Dependent type variables]
1300
1301 , dv_cvs :: CoVarSet
1302 -- These are covars. Included only so that we don't repeatedly
1303 -- look at covars' kinds in accumulator. Not used by quantifyTyVars.
1304 }
1305
1306 instance Semi.Semigroup CandidatesQTvs where
1307 (DV { dv_kvs = kv1, dv_tvs = tv1, dv_cvs = cv1 })
1308 <> (DV { dv_kvs = kv2, dv_tvs = tv2, dv_cvs = cv2 })
1309 = DV { dv_kvs = kv1 `unionDVarSet` kv2
1310 , dv_tvs = tv1 `unionDVarSet` tv2
1311 , dv_cvs = cv1 `unionVarSet` cv2 }
1312
1313 instance Monoid CandidatesQTvs where
1314 mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet, dv_cvs = emptyVarSet }
1315 mappend = (Semi.<>)
1316
1317 instance Outputable CandidatesQTvs where
1318 ppr (DV {dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs })
1319 = text "DV" <+> braces (pprWithCommas id [ text "dv_kvs =" <+> ppr kvs
1320 , text "dv_tvs =" <+> ppr tvs
1321 , text "dv_cvs =" <+> ppr cvs ])
1322
1323 isEmptyCandidates :: CandidatesQTvs -> Bool
1324 isEmptyCandidates (DV { dv_kvs = kvs, dv_tvs = tvs })
1325 = isEmptyDVarSet kvs && isEmptyDVarSet tvs
1326
1327 -- | Extract out the kind vars (in order) and type vars (in order) from
1328 -- a 'CandidatesQTvs'. The lists are guaranteed to be distinct. Keeping
1329 -- the lists separate is important only in the -XNoPolyKinds case.
1330 candidateVars :: CandidatesQTvs -> ([TcTyVar], [TcTyVar])
1331 candidateVars (DV { dv_kvs = dep_kv_set, dv_tvs = nondep_tkv_set })
1332 = (dep_kvs, nondep_tvs)
1333 where
1334 dep_kvs = scopedSort $ dVarSetElems dep_kv_set
1335 -- scopedSort: put the kind variables into
1336 -- well-scoped order.
1337 -- E.g. [k, (a::k)] not the other way round
1338
1339 nondep_tvs = dVarSetElems (nondep_tkv_set `minusDVarSet` dep_kv_set)
1340 -- See Note [Dependent type variables]
1341 -- The `minus` dep_tkvs removes any kind-level vars
1342 -- e.g. T k (a::k) Since k appear in a kind it'll
1343 -- be in dv_kvs, and is dependent. So remove it from
1344 -- dv_tvs which will also contain k
1345 -- NB kinds of tvs are already zonked
1346
1347 candidateKindVars :: CandidatesQTvs -> TyVarSet
1348 candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs)
1349
1350 partitionCandidates :: CandidatesQTvs -> (TyVar -> Bool) -> (TyVarSet, CandidatesQTvs)
1351 -- The selected TyVars are returned as a non-deterministic TyVarSet
1352 partitionCandidates dvs@(DV { dv_kvs = kvs, dv_tvs = tvs }) pred
1353 = (extracted, dvs { dv_kvs = rest_kvs, dv_tvs = rest_tvs })
1354 where
1355 (extracted_kvs, rest_kvs) = partitionDVarSet pred kvs
1356 (extracted_tvs, rest_tvs) = partitionDVarSet pred tvs
1357 extracted = dVarSetToVarSet extracted_kvs `unionVarSet` dVarSetToVarSet extracted_tvs
1358
1359 -- | Gathers free variables to use as quantification candidates (in
1360 -- 'quantifyTyVars'). This might output the same var
1361 -- in both sets, if it's used in both a type and a kind.
1362 -- The variables to quantify must have a TcLevel strictly greater than
1363 -- the ambient level. (See Wrinkle in Note [Naughty quantification candidates])
1364 -- See Note [CandidatesQTvs determinism and order]
1365 -- See Note [Dependent type variables]
1366 candidateQTyVarsOfType :: TcType -- not necessarily zonked
1367 -> TcM CandidatesQTvs
1368 candidateQTyVarsOfType ty = collect_cand_qtvs ty False emptyVarSet mempty ty
1369
1370 -- | Like 'candidateQTyVarsOfType', but over a list of types
1371 -- The variables to quantify must have a TcLevel strictly greater than
1372 -- the ambient level. (See Wrinkle in Note [Naughty quantification candidates])
1373 candidateQTyVarsOfTypes :: [Type] -> TcM CandidatesQTvs
1374 candidateQTyVarsOfTypes tys = foldlM (\acc ty -> collect_cand_qtvs ty False emptyVarSet acc ty)
1375 mempty tys
1376
1377 -- | Like 'candidateQTyVarsOfType', but consider every free variable
1378 -- to be dependent. This is appropriate when generalizing a *kind*,
1379 -- instead of a type. (That way, -XNoPolyKinds will default the variables
1380 -- to Type.)
1381 candidateQTyVarsOfKind :: TcKind -- Not necessarily zonked
1382 -> TcM CandidatesQTvs
1383 candidateQTyVarsOfKind ty = collect_cand_qtvs ty True emptyVarSet mempty ty
1384
1385 candidateQTyVarsOfKinds :: [TcKind] -- Not necessarily zonked
1386 -> TcM CandidatesQTvs
1387 candidateQTyVarsOfKinds tys = foldM (\acc ty -> collect_cand_qtvs ty True emptyVarSet acc ty)
1388 mempty tys
1389
1390 delCandidates :: CandidatesQTvs -> [Var] -> CandidatesQTvs
1391 delCandidates (DV { dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) vars
1392 = DV { dv_kvs = kvs `delDVarSetList` vars
1393 , dv_tvs = tvs `delDVarSetList` vars
1394 , dv_cvs = cvs `delVarSetList` vars }
1395
1396 collect_cand_qtvs
1397 :: TcType -- original type that we started recurring into; for errors
1398 -> Bool -- True <=> consider every fv in Type to be dependent
1399 -> VarSet -- Bound variables (locals only)
1400 -> CandidatesQTvs -- Accumulating parameter
1401 -> Type -- Not necessarily zonked
1402 -> TcM CandidatesQTvs
1403
1404 -- Key points:
1405 -- * Looks through meta-tyvars as it goes;
1406 -- no need to zonk in advance
1407 --
1408 -- * Needs to be monadic anyway, because it handles naughty
1409 -- quantification; see Note [Naughty quantification candidates]
1410 --
1411 -- * Returns fully-zonked CandidateQTvs, including their kinds
1412 -- so that subsequent dependency analysis (to build a well
1413 -- scoped telescope) works correctly
1414
1415 collect_cand_qtvs orig_ty is_dep bound dvs ty
1416 = go dvs ty
1417 where
1418 is_bound tv = tv `elemVarSet` bound
1419
1420 -----------------
1421 go :: CandidatesQTvs -> TcType -> TcM CandidatesQTvs
1422 -- Uses accumulating-parameter style
1423 go dv (AppTy t1 t2) = foldlM go dv [t1, t2]
1424 go dv (TyConApp tc tys) = go_tc_args dv (tyConBinders tc) tys
1425 go dv (FunTy _ w arg res) = foldlM go dv [w, arg, res]
1426 go dv (LitTy {}) = return dv
1427 go dv (CastTy ty co) = do dv1 <- go dv ty
1428 collect_cand_qtvs_co orig_ty bound dv1 co
1429 go dv (CoercionTy co) = collect_cand_qtvs_co orig_ty bound dv co
1430
1431 go dv (TyVarTy tv)
1432 | is_bound tv = return dv
1433 | otherwise = do { m_contents <- isFilledMetaTyVar_maybe tv
1434 ; case m_contents of
1435 Just ind_ty -> go dv ind_ty
1436 Nothing -> go_tv dv tv }
1437
1438 go dv (ForAllTy (Bndr tv _) ty)
1439 = do { dv1 <- collect_cand_qtvs orig_ty True bound dv (tyVarKind tv)
1440 ; collect_cand_qtvs orig_ty is_dep (bound `extendVarSet` tv) dv1 ty }
1441
1442 -- This makes sure that we default e.g. the alpha in Proxy alpha (Any alpha).
1443 -- Tested in polykinds/NestedProxies.
1444 -- We just might get this wrong in AppTy, but I don't think that's possible
1445 -- with -XNoPolyKinds. And fixing it would be non-performant, as we'd need
1446 -- to look at kinds.
1447 go_tc_args dv (tc_bndr:tc_bndrs) (ty:tys)
1448 = do { dv1 <- collect_cand_qtvs orig_ty (is_dep || isNamedTyConBinder tc_bndr)
1449 bound dv ty
1450 ; go_tc_args dv1 tc_bndrs tys }
1451 go_tc_args dv _bndrs tys -- _bndrs might be non-empty: undersaturation
1452 -- tys might be non-empty: oversaturation
1453 -- either way, the foldlM is correct
1454 = foldlM go dv tys
1455
1456 -----------------
1457 go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv
1458 | tv `elemDVarSet` kvs
1459 = return dv -- We have met this tyvar already
1460
1461 | not is_dep
1462 , tv `elemDVarSet` tvs
1463 = return dv -- We have met this tyvar already
1464
1465 | otherwise
1466 = do { tv_kind <- zonkTcType (tyVarKind tv)
1467 -- This zonk is annoying, but it is necessary, both to
1468 -- ensure that the collected candidates have zonked kinds
1469 -- (#15795) and to make the naughty check
1470 -- (which comes next) works correctly
1471
1472 ; let tv_kind_vars = tyCoVarsOfType tv_kind
1473 ; cur_lvl <- getTcLevel
1474 ; if | tcTyVarLevel tv <= cur_lvl
1475 -> return dv -- this variable is from an outer context; skip
1476 -- See Note [Use level numbers for quantification]
1477
1478 | intersectsVarSet bound tv_kind_vars
1479 -- the tyvar must not be from an outer context, but we have
1480 -- already checked for this.
1481 -- See Note [Naughty quantification candidates]
1482 -> do { traceTc "Naughty quantifier" $
1483 vcat [ ppr tv <+> dcolon <+> ppr tv_kind
1484 , text "bound:" <+> pprTyVars (nonDetEltsUniqSet bound)
1485 , text "fvs:" <+> pprTyVars (nonDetEltsUniqSet tv_kind_vars) ]
1486
1487 ; let escapees = intersectVarSet bound tv_kind_vars
1488 ; naughtyQuantification orig_ty tv escapees }
1489
1490 | otherwise
1491 -> do { let tv' = tv `setTyVarKind` tv_kind
1492 dv' | is_dep = dv { dv_kvs = kvs `extendDVarSet` tv' }
1493 | otherwise = dv { dv_tvs = tvs `extendDVarSet` tv' }
1494 -- See Note [Order of accumulation]
1495
1496 -- See Note [Recurring into kinds for candidateQTyVars]
1497 ; collect_cand_qtvs orig_ty True bound dv' tv_kind } }
1498
1499 collect_cand_qtvs_co :: TcType -- original type at top of recursion; for errors
1500 -> VarSet -- bound variables
1501 -> CandidatesQTvs -> Coercion
1502 -> TcM CandidatesQTvs
1503 collect_cand_qtvs_co orig_ty bound = go_co
1504 where
1505 go_co dv (Refl ty) = collect_cand_qtvs orig_ty True bound dv ty
1506 go_co dv (GRefl _ ty mco) = do dv1 <- collect_cand_qtvs orig_ty True bound dv ty
1507 go_mco dv1 mco
1508 go_co dv (TyConAppCo _ _ cos) = foldlM go_co dv cos
1509 go_co dv (AppCo co1 co2) = foldlM go_co dv [co1, co2]
1510 go_co dv (FunCo _ w co1 co2) = foldlM go_co dv [w, co1, co2]
1511 go_co dv (AxiomInstCo _ _ cos) = foldlM go_co dv cos
1512 go_co dv (AxiomRuleCo _ cos) = foldlM go_co dv cos
1513 go_co dv (UnivCo prov _ t1 t2) = do dv1 <- go_prov dv prov
1514 dv2 <- collect_cand_qtvs orig_ty True bound dv1 t1
1515 collect_cand_qtvs orig_ty True bound dv2 t2
1516 go_co dv (SymCo co) = go_co dv co
1517 go_co dv (TransCo co1 co2) = foldlM go_co dv [co1, co2]
1518 go_co dv (NthCo _ _ co) = go_co dv co
1519 go_co dv (LRCo _ co) = go_co dv co
1520 go_co dv (InstCo co1 co2) = foldlM go_co dv [co1, co2]
1521 go_co dv (KindCo co) = go_co dv co
1522 go_co dv (SubCo co) = go_co dv co
1523
1524 go_co dv (HoleCo hole)
1525 = do m_co <- unpackCoercionHole_maybe hole
1526 case m_co of
1527 Just co -> go_co dv co
1528 Nothing -> go_cv dv (coHoleCoVar hole)
1529
1530 go_co dv (CoVarCo cv) = go_cv dv cv
1531
1532 go_co dv (ForAllCo tcv kind_co co)
1533 = do { dv1 <- go_co dv kind_co
1534 ; collect_cand_qtvs_co orig_ty (bound `extendVarSet` tcv) dv1 co }
1535
1536 go_mco dv MRefl = return dv
1537 go_mco dv (MCo co) = go_co dv co
1538
1539 go_prov dv (PhantomProv co) = go_co dv co
1540 go_prov dv (ProofIrrelProv co) = go_co dv co
1541 go_prov dv (PluginProv _) = return dv
1542 go_prov dv (CorePrepProv _) = return dv
1543
1544 go_cv :: CandidatesQTvs -> CoVar -> TcM CandidatesQTvs
1545 go_cv dv@(DV { dv_cvs = cvs }) cv
1546 | is_bound cv = return dv
1547 | cv `elemVarSet` cvs = return dv
1548
1549 -- See Note [Recurring into kinds for candidateQTyVars]
1550 | otherwise = collect_cand_qtvs orig_ty True bound
1551 (dv { dv_cvs = cvs `extendVarSet` cv })
1552 (idType cv)
1553
1554 is_bound tv = tv `elemVarSet` bound
1555
1556 {- Note [Order of accumulation]
1557 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1558 You might be tempted (like I was) to use unitDVarSet and mappend
1559 rather than extendDVarSet. However, the union algorithm for
1560 deterministic sets depends on (roughly) the size of the sets. The
1561 elements from the smaller set end up to the right of the elements from
1562 the larger one. When sets are equal, the left-hand argument to
1563 `mappend` goes to the right of the right-hand argument.
1564
1565 In our case, if we use unitDVarSet and mappend, we learn that the free
1566 variables of (a -> b -> c -> d) are [b, a, c, d], and we then quantify
1567 over them in that order. (The a comes after the b because we union the
1568 singleton sets as ({a} `mappend` {b}), producing {b, a}. Thereafter,
1569 the size criterion works to our advantage.) This is just annoying to
1570 users, so I use `extendDVarSet`, which unambiguously puts the new
1571 element to the right.
1572
1573 Note that the unitDVarSet/mappend implementation would not be wrong
1574 against any specification -- just suboptimal and confounding to users.
1575
1576 Note [Recurring into kinds for candidateQTyVars]
1577 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1578 First, read Note [Closing over free variable kinds] in GHC.Core.TyCo.FVs, paying
1579 attention to the end of the Note about using an empty bound set when
1580 traversing a variable's kind.
1581
1582 That Note concludes with the recommendation that we empty out the bound
1583 set when recurring into the kind of a type variable. Yet, we do not do
1584 this here. I have two tasks in order to convince you that this code is
1585 right. First, I must show why it is safe to ignore the reasoning in that
1586 Note. Then, I must show why is is necessary to contradict the reasoning in
1587 that Note.
1588
1589 Why it is safe: There can be no
1590 shadowing in the candidateQ... functions: they work on the output of
1591 type inference, which is seeded by the renamer and its insistence to
1592 use different Uniques for different variables. (In contrast, the Core
1593 functions work on the output of optimizations, which may introduce
1594 shadowing.) Without shadowing, the problem studied by
1595 Note [Closing over free variable kinds] in GHC.Core.TyCo.FVs cannot happen.
1596
1597 Why it is necessary:
1598 Wiping the bound set would be just plain wrong here. Consider
1599
1600 forall k1 k2 (a :: k1). Proxy k2 (a |> (hole :: k1 ~# k2))
1601
1602 We really don't want to think k1 and k2 are free here. (It's true that we'll
1603 never be able to fill in `hole`, but we don't want to go off the rails just
1604 because we have an insoluble coercion hole.) So: why is it wrong to wipe
1605 the bound variables here but right in Core? Because the final statement
1606 in Note [Closing over free variable kinds] in GHC.Core.TyCo.FVs is wrong: not
1607 every variable is either free or bound. A variable can be a hole, too!
1608 The reasoning in that Note then breaks down.
1609
1610 And the reasoning applies just as well to free non-hole variables, so we
1611 retain the bound set always.
1612
1613 -}
1614
1615 {- *********************************************************************
1616 * *
1617 Quantification
1618 * *
1619 ************************************************************************
1620
1621 Note [quantifyTyVars]
1622 ~~~~~~~~~~~~~~~~~~~~~
1623 quantifyTyVars is given the free vars of a type that we
1624 are about to wrap in a forall.
1625
1626 It takes these free type/kind variables (partitioned into dependent and
1627 non-dependent variables) skolemises metavariables with a TcLevel greater
1628 than the ambient level (see Note [Use level numbers for quantification]).
1629
1630 * This function distinguishes between dependent and non-dependent
1631 variables only to keep correct defaulting behavior with -XNoPolyKinds.
1632 With -XPolyKinds, it treats both classes of variables identically.
1633
1634 * quantifyTyVars never quantifies over
1635 - a coercion variable (or any tv mentioned in the kind of a covar)
1636 - a runtime-rep variable
1637
1638 Note [Use level numbers for quantification]
1639 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1640 The level numbers assigned to metavariables are very useful. Not only
1641 do they track touchability (Note [TcLevel invariants] in GHC.Tc.Utils.TcType),
1642 but they also allow us to determine which variables to
1643 generalise. The rule is this:
1644
1645 When generalising, quantify only metavariables with a TcLevel greater
1646 than the ambient level.
1647
1648 This works because we bump the level every time we go inside a new
1649 source-level construct. In a traditional generalisation algorithm, we
1650 would gather all free variables that aren't free in an environment.
1651 However, if a variable is in that environment, it will always have a lower
1652 TcLevel: it came from an outer scope. So we can replace the "free in
1653 environment" check with a level-number check.
1654
1655 Here is an example:
1656
1657 f x = x + (z True)
1658 where
1659 z y = x * x
1660
1661 We start by saying (x :: alpha[1]). When inferring the type of z, we'll
1662 quickly discover that z :: alpha[1]. But it would be disastrous to
1663 generalise over alpha in the type of z. So we need to know that alpha
1664 comes from an outer environment. By contrast, the type of y is beta[2],
1665 and we are free to generalise over it. What's the difference between
1666 alpha[1] and beta[2]? Their levels. beta[2] has the right TcLevel for
1667 generalisation, and so we generalise it. alpha[1] does not, and so
1668 we leave it alone.
1669
1670 Note that not *every* variable with a higher level will get
1671 generalised, either due to the monomorphism restriction or other
1672 quirks. See, for example, the code in GHC.Tc.Solver.decideMonoTyVars
1673 and in GHC.Tc.Gen.HsType.kindGeneralizeSome, both of which exclude
1674 certain otherwise-eligible variables from being generalised.
1675
1676 Using level numbers for quantification is implemented in the candidateQTyVars...
1677 functions, by adding only those variables with a level strictly higher than
1678 the ambient level to the set of candidates.
1679
1680 Note [quantifyTyVars determinism]
1681 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1682 The results of quantifyTyVars are wrapped in a forall and can end up in the
1683 interface file. One such example is inferred type signatures. They also affect
1684 the results of optimizations, for example worker-wrapper. This means that to
1685 get deterministic builds quantifyTyVars needs to be deterministic.
1686
1687 To achieve this CandidatesQTvs is backed by deterministic sets which allows them
1688 to be later converted to a list in a deterministic order.
1689
1690 For more information about deterministic sets see
1691 Note [Deterministic UniqFM] in GHC.Types.Unique.DFM.
1692 -}
1693
1694 quantifyTyVars :: DefaultVarsOfKind
1695 -> CandidatesQTvs -- See Note [Dependent type variables]
1696 -- Already zonked
1697 -> TcM [TcTyVar]
1698 -- See Note [quantifyTyVars]
1699 -- Can be given a mixture of TcTyVars and TyVars, in the case of
1700 -- associated type declarations. Also accepts covars, but *never* returns any.
1701 -- According to Note [Use level numbers for quantification] and the
1702 -- invariants on CandidateQTvs, we do not have to filter out variables
1703 -- free in the environment here. Just quantify unconditionally, subject
1704 -- to the restrictions in Note [quantifyTyVars].
1705 quantifyTyVars def_varsOfKind dvs
1706 -- short-circuit common case
1707 | isEmptyCandidates dvs
1708 = do { traceTc "quantifyTyVars has nothing to quantify" empty
1709 ; return [] }
1710
1711 | otherwise
1712 = do { traceTc "quantifyTyVars {"
1713 ( vcat [ text "def_varsOfKind =" <+> ppr def_varsOfKind
1714 , text "dvs =" <+> ppr dvs ])
1715
1716 ; undefaulted <- defaultTyVars def_varsOfKind dvs
1717 ; final_qtvs <- mapMaybeM zonk_quant undefaulted
1718
1719 ; traceTc "quantifyTyVars }"
1720 (vcat [ text "undefaulted:" <+> pprTyVars undefaulted
1721 , text "final_qtvs:" <+> pprTyVars final_qtvs ])
1722
1723 -- We should never quantify over coercion variables; check this
1724 ; let co_vars = filter isCoVar final_qtvs
1725 ; massertPpr (null co_vars) (ppr co_vars)
1726
1727 ; return final_qtvs }
1728 where
1729 -- zonk_quant returns a tyvar if it should be quantified over;
1730 -- otherwise, it returns Nothing. The latter case happens for
1731 -- non-meta-tyvars
1732 zonk_quant tkv
1733 | not (isTyVar tkv)
1734 = return Nothing -- this can happen for a covar that's associated with
1735 -- a coercion hole. Test case: typecheck/should_compile/T2494
1736
1737 | not (isTcTyVar tkv)
1738 = return (Just tkv) -- For associated types in a class with a standalone
1739 -- kind signature, we have the class variables in
1740 -- scope, and they are TyVars not TcTyVars
1741 | otherwise
1742 = Just <$> skolemiseQuantifiedTyVar tkv
1743
1744 isQuantifiableTv :: TcLevel -- Level of the context, outside the quantification
1745 -> TcTyVar
1746 -> Bool
1747 isQuantifiableTv outer_tclvl tcv
1748 | isTcTyVar tcv -- Might be a CoVar; change this when gather covars separately
1749 = tcTyVarLevel tcv > outer_tclvl
1750 | otherwise
1751 = False
1752
1753 zonkAndSkolemise :: TcTyCoVar -> TcM TcTyCoVar
1754 -- A tyvar binder is never a unification variable (TauTv),
1755 -- rather it is always a skolem. It *might* be a TyVarTv.
1756 -- (Because non-CUSK type declarations use TyVarTvs.)
1757 -- Regardless, it may have a kind that has not yet been zonked,
1758 -- and may include kind unification variables.
1759 zonkAndSkolemise tyvar
1760 | isTyVarTyVar tyvar
1761 -- We want to preserve the binding location of the original TyVarTv.
1762 -- This is important for error messages. If we don't do this, then
1763 -- we get bad locations in, e.g., typecheck/should_fail/T2688
1764 = do { zonked_tyvar <- zonkTcTyVarToTyVar tyvar
1765 ; skolemiseQuantifiedTyVar zonked_tyvar }
1766
1767 | otherwise
1768 = assertPpr (isImmutableTyVar tyvar || isCoVar tyvar) (pprTyVar tyvar) $
1769 zonkTyCoVarKind tyvar
1770
1771 skolemiseQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
1772 -- The quantified type variables often include meta type variables
1773 -- we want to freeze them into ordinary type variables
1774 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
1775 -- bound occurrences of the original type variable will get zonked to
1776 -- the immutable version.
1777 --
1778 -- We leave skolem TyVars alone; they are immutable.
1779 --
1780 -- This function is called on both kind and type variables,
1781 -- but kind variables *only* if PolyKinds is on.
1782
1783 skolemiseQuantifiedTyVar tv
1784 = case tcTyVarDetails tv of
1785 SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
1786 ; return (setTyVarKind tv kind) }
1787 -- It might be a skolem type variable,
1788 -- for example from a user type signature
1789
1790 MetaTv {} -> skolemiseUnboundMetaTyVar tv
1791
1792 _other -> pprPanic "skolemiseQuantifiedTyVar" (ppr tv) -- RuntimeUnk
1793
1794 defaultTyVar :: DefaultKindVars
1795 -> DefaultVarsOfKind
1796 -> TcTyVar -- If it's a MetaTyVar then it is unbound
1797 -> TcM Bool -- True <=> defaulted away altogether
1798
1799 defaultTyVar def_kindVars def_varsOfKind tv
1800 | not (isMetaTyVar tv)
1801 = return False
1802
1803 | isTyVarTyVar tv
1804 -- Do not default TyVarTvs. Doing so would violate the invariants
1805 -- on TyVarTvs; see Note [TyVarTv] in GHC.Tc.Utils.TcMType.
1806 -- #13343 is an example; #14555 is another
1807 -- See Note [Inferring kinds for type declarations] in GHC.Tc.TyCl
1808 = return False
1809
1810
1811 | isRuntimeRepVar tv
1812 , def_runtimeRep def_varsOfKind
1813 -- Do not quantify over a RuntimeRep var
1814 -- unless it is a TyVarTv, handled earlier
1815 = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
1816 ; writeMetaTyVar tv liftedRepTy
1817 ; return True }
1818 | isLevityVar tv
1819 , def_levity def_varsOfKind
1820 = do { traceTc "Defaulting a Levity var to Lifted" (ppr tv)
1821 ; writeMetaTyVar tv liftedDataConTy
1822 ; return True }
1823 | isMultiplicityVar tv
1824 , def_multiplicity def_varsOfKind
1825 = do { traceTc "Defaulting a Multiplicty var to Many" (ppr tv)
1826 ; writeMetaTyVar tv manyDataConTy
1827 ; return True }
1828
1829 | DefaultKinds <- def_kindVars -- -XNoPolyKinds and this is a kind var
1830 = default_kind_var tv -- so default it to * if possible
1831
1832 | otherwise
1833 = return False
1834
1835 where
1836 default_kind_var :: TyVar -> TcM Bool
1837 -- defaultKindVar is used exclusively with -XNoPolyKinds
1838 -- See Note [Defaulting with -XNoPolyKinds]
1839 -- It takes an (unconstrained) meta tyvar and defaults it.
1840 -- Works only on vars of type *; for other kinds, it issues an error.
1841 default_kind_var kv
1842 | isLiftedTypeKind (tyVarKind kv)
1843 = do { traceTc "Defaulting a kind var to *" (ppr kv)
1844 ; writeMetaTyVar kv liftedTypeKind
1845 ; return True }
1846 | otherwise
1847 = do { addErr $ TcRnUnknownMessage $ mkPlainError noHints $
1848 (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
1849 , text "of kind:" <+> ppr (tyVarKind kv')
1850 , text "Perhaps enable PolyKinds or add a kind signature" ])
1851 -- We failed to default it, so return False to say so.
1852 -- Hence, it'll get skolemised. That might seem odd, but we must either
1853 -- promote, skolemise, or zap-to-Any, to satisfy GHC.Tc.Gen.HsType
1854 -- Note [Recipe for checking a signature]
1855 -- Otherwise we get level-number assertion failures. It doesn't matter much
1856 -- because we are in an error situation anyway.
1857 ; return False
1858 }
1859 where
1860 (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
1861
1862 -- | Default some unconstrained type variables:
1863 -- RuntimeRep tyvars default to LiftedRep
1864 -- Multiplicity tyvars default to Many
1865 -- Type tyvars from dv_kvs default to Type, when -XNoPolyKinds
1866 -- (under -XNoPolyKinds, non-defaulting vars in dv_kvs is an error)
1867 defaultTyVars :: DefaultVarsOfKind
1868 -> CandidatesQTvs -- ^ all candidates for quantification
1869 -> TcM [TcTyVar] -- ^ those variables not defaulted
1870 defaultTyVars def_varsOfKind dvs
1871 = do { poly_kinds <- xoptM LangExt.PolyKinds
1872 ; let
1873 def_kinds = if poly_kinds then Don'tDefaultKinds else DefaultKinds
1874 ; defaulted_kvs <- mapM (defaultTyVar def_kinds def_varsOfKind ) dep_kvs
1875 ; defaulted_tvs <- mapM (defaultTyVar Don'tDefaultKinds def_varsOfKind ) nondep_tvs
1876 ; let undefaulted_kvs = [ kv | (kv, False) <- dep_kvs `zip` defaulted_kvs ]
1877 undefaulted_tvs = [ tv | (tv, False) <- nondep_tvs `zip` defaulted_tvs ]
1878 ; return (undefaulted_kvs ++ undefaulted_tvs) }
1879 -- NB: kvs before tvs because tvs may depend on kvs
1880 where
1881 (dep_kvs, nondep_tvs) = candidateVars dvs
1882
1883 skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar
1884 -- We have a Meta tyvar with a ref-cell inside it
1885 -- Skolemise it, so that we are totally out of Meta-tyvar-land
1886 -- We create a skolem TcTyVar, not a regular TyVar
1887 -- See Note [Zonking to Skolem]
1888 skolemiseUnboundMetaTyVar tv
1889 = assertPpr (isMetaTyVar tv) (ppr tv) $
1890 do { when debugIsOn (check_empty tv)
1891 ; here <- getSrcSpanM -- Get the location from "here"
1892 -- ie where we are generalising
1893 ; kind <- zonkTcType (tyVarKind tv)
1894 ; let tv_name = tyVarName tv
1895 -- See Note [Skolemising and identity]
1896 final_name | isSystemName tv_name
1897 = mkInternalName (nameUnique tv_name)
1898 (nameOccName tv_name) here
1899 | otherwise
1900 = tv_name
1901 final_tv = mkTcTyVar final_name kind details
1902
1903 ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
1904 ; writeMetaTyVar tv (mkTyVarTy final_tv)
1905 ; return final_tv }
1906
1907 where
1908 details = SkolemTv (metaTyVarTcLevel tv) False
1909 check_empty tv -- [Sept 04] Check for non-empty.
1910 = when debugIsOn $ -- See note [Silly Type Synonym]
1911 do { cts <- readMetaTyVar tv
1912 ; case cts of
1913 Flexi -> return ()
1914 Indirect ty -> warnPprTrace True (ppr tv $$ ppr ty) $
1915 return () }
1916
1917 {- Note [Error on unconstrained meta-variables]
1918 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1919 Consider
1920
1921 type C :: Type -> Type -> Constraint
1922 class (forall a. a b ~ a c) => C b c
1923
1924 or
1925
1926 type T = forall a. Proxy a
1927
1928 or
1929
1930 data (forall a. a b ~ a c) => T b c
1931
1932 We will infer a :: Type -> kappa... but then we get no further information
1933 on kappa. What to do?
1934
1935 A. We could choose kappa := Type. But this only works when the kind of kappa
1936 is Type (true in this example, but not always).
1937 B. We could default to Any.
1938 C. We could quantify.
1939 D. We could error.
1940
1941 We choose (D), as described in #17567. Discussion of alternatives is below.
1942
1943 NB: this is all rather similar to, but sadly not the same as
1944 Note [Naughty quantification candidates]
1945
1946 (One last example: type instance F Int = Proxy Any, where the unconstrained
1947 kind variable is the inferred kind of Any. The four examples here illustrate
1948 all cases in which this Note applies.)
1949
1950 To do this, we must take an extra step before doing the final zonk to create
1951 e.g. a TyCon. (There is no problem in the final term-level zonk. See the
1952 section on alternative (B) below.) This extra step is needed only for
1953 constructs that do not quantify their free meta-variables, such as a class
1954 constraint or right-hand side of a type synonym.
1955
1956 Specifically: before the final zonk, every construct must either call
1957 quantifyTyVars or doNotQuantifyTyVars. The latter issues an error
1958 if it is passed any free variables. (Exception: we still default
1959 RuntimeRep and Multiplicity variables.)
1960
1961 Because no meta-variables remain after quantifying or erroring, we perform
1962 the zonk with NoFlexi, which panics upon seeing a meta-variable.
1963
1964 Alternatives not implemented:
1965
1966 A. As stated above, this works only sometimes. We might have a free
1967 meta-variable of kind Nat, for example.
1968
1969 B. This is what we used to do, but it caused Any to appear in error
1970 messages sometimes. See #17567 for several examples. Defaulting to
1971 Any during the final, whole-program zonk is OK, though, because
1972 we are completely done type-checking at that point. No chance to
1973 leak into an error message.
1974
1975 C. Examine the class declaration at the top of this Note again.
1976 Where should we quantify? We might imagine quantifying and
1977 putting the kind variable in the forall of the quantified constraint.
1978 But what if there are nested foralls? Which one should get the
1979 variable? Other constructs have other problems. (For example,
1980 the right-hand side of a type family instance equation may not
1981 be a poly-type.)
1982
1983 More broadly, the GHC AST defines a set of places where it performs
1984 implicit lexical generalization. For example, in a type
1985 signature
1986
1987 f :: Proxy a -> Bool
1988
1989 the otherwise-unbound a is lexically quantified, giving us
1990
1991 f :: forall a. Proxy a -> Bool
1992
1993 The places that allow lexical quantification are marked in the AST with
1994 HsImplicitBndrs. HsImplicitBndrs offers a binding site for otherwise-unbound
1995 variables.
1996
1997 Later, during type-checking, we discover that a's kind is unconstrained.
1998 We thus quantify *again*, to
1999
2000 f :: forall {k} (a :: k). Proxy @k a -> Bool
2001
2002 It is this second quantification that this Note is really about --
2003 let's call it *inferred quantification*.
2004 So there are two sorts of implicit quantification in types:
2005 1. Lexical quantification: signalled by HsImplicitBndrs, occurs over
2006 variables mentioned by the user but with no explicit binding site,
2007 suppressed by a user-written forall (by the forall-or-nothing rule,
2008 in Note [forall-or-nothing rule] in GHC.Hs.Type).
2009 2. Inferred quantification: no signal in HsSyn, occurs over unconstrained
2010 variables invented by the type-checker, possible only with -XPolyKinds,
2011 unaffected by forall-or-nothing rule
2012 These two quantifications are performed in different compiler phases, and are
2013 essentially unrelated. However, it is convenient
2014 for programmers to remember only one set of implicit quantification
2015 sites. So, we choose to use the same places (those with HsImplicitBndrs)
2016 for lexical quantification as for inferred quantification of unconstrained
2017 meta-variables. Accordingly, there is no quantification in a class
2018 constraint, or the other constructs that call doNotQuantifyTyVars.
2019 -}
2020
2021 doNotQuantifyTyVars :: CandidatesQTvs
2022 -> (TidyEnv -> TcM (TidyEnv, SDoc))
2023 -- ^ like "the class context (D a b, E foogle)"
2024 -> TcM ()
2025 -- See Note [Error on unconstrained meta-variables]
2026 doNotQuantifyTyVars dvs where_found
2027 | isEmptyCandidates dvs
2028 = traceTc "doNotQuantifyTyVars has nothing to error on" empty
2029
2030 | otherwise
2031 = do { traceTc "doNotQuantifyTyVars" (ppr dvs)
2032 ; undefaulted <- defaultTyVars allVarsOfKindDefault dvs
2033 -- could have regular TyVars here, in an associated type RHS, or
2034 -- bound by a type declaration head. So filter looking only for
2035 -- metavars. e.g. b and c in `class (forall a. a b ~ a c) => C b c`
2036 -- are OK
2037 ; let leftover_metas = filter isMetaTyVar undefaulted
2038 ; unless (null leftover_metas) $
2039 do { let (tidy_env1, tidied_tvs) = tidyOpenTyCoVars emptyTidyEnv leftover_metas
2040 ; (tidy_env2, where_doc) <- where_found tidy_env1
2041 ; let msg = TcRnUnknownMessage $ mkPlainError noHints $ pprWithExplicitKindsWhen True $
2042 vcat [ text "Uninferrable type variable"
2043 <> plural tidied_tvs
2044 <+> pprWithCommas pprTyVar tidied_tvs
2045 <+> text "in"
2046 , where_doc ]
2047 ; failWithTcM (tidy_env2, msg) }
2048 ; traceTc "doNotQuantifyTyVars success" empty }
2049
2050 {- Note [Defaulting with -XNoPolyKinds]
2051 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2052 Consider
2053
2054 data Compose f g a = Mk (f (g a))
2055
2056 We infer
2057
2058 Compose :: forall k1 k2. (k2 -> *) -> (k1 -> k2) -> k1 -> *
2059 Mk :: forall k1 k2 (f :: k2 -> *) (g :: k1 -> k2) (a :: k1).
2060 f (g a) -> Compose k1 k2 f g a
2061
2062 Now, in another module, we have -XNoPolyKinds -XDataKinds in effect.
2063 What does 'Mk mean? Pre GHC-8.0 with -XNoPolyKinds,
2064 we just defaulted all kind variables to *. But that's no good here,
2065 because the kind variables in 'Mk aren't of kind *, so defaulting to *
2066 is ill-kinded.
2067
2068 After some debate on #11334, we decided to issue an error in this case.
2069 The code is in defaultKindVar.
2070
2071 Note [What is a meta variable?]
2072 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2073 A "meta type-variable", also know as a "unification variable" is a placeholder
2074 introduced by the typechecker for an as-yet-unknown monotype.
2075
2076 For example, when we see a call `reverse (f xs)`, we know that we calling
2077 reverse :: forall a. [a] -> [a]
2078 So we know that the argument `f xs` must be a "list of something". But what is
2079 the "something"? We don't know until we explore the `f xs` a bit more. So we set
2080 out what we do know at the call of `reverse` by instantiating its type with a fresh
2081 meta tyvar, `alpha` say. So now the type of the argument `f xs`, and of the
2082 result, is `[alpha]`. The unification variable `alpha` stands for the
2083 as-yet-unknown type of the elements of the list.
2084
2085 As type inference progresses we may learn more about `alpha`. For example, suppose
2086 `f` has the type
2087 f :: forall b. b -> [Maybe b]
2088 Then we instantiate `f`'s type with another fresh unification variable, say
2089 `beta`; and equate `f`'s result type with reverse's argument type, thus
2090 `[alpha] ~ [Maybe beta]`.
2091
2092 Now we can solve this equality to learn that `alpha ~ Maybe beta`, so we've
2093 refined our knowledge about `alpha`. And so on.
2094
2095 If you found this Note useful, you may also want to have a look at
2096 Section 5 of "Practical type inference for higher rank types" (Peyton Jones,
2097 Vytiniotis, Weirich and Shields. J. Functional Programming. 2011).
2098
2099 Note [What is zonking?]
2100 ~~~~~~~~~~~~~~~~~~~~~~~
2101 GHC relies heavily on mutability in the typechecker for efficient operation.
2102 For this reason, throughout much of the type checking process meta type
2103 variables (the MetaTv constructor of TcTyVarDetails) are represented by mutable
2104 variables (known as TcRefs).
2105
2106 Zonking is the process of ripping out these mutable variables and replacing them
2107 with a real Type. This involves traversing the entire type expression, but the
2108 interesting part of replacing the mutable variables occurs in zonkTyVarOcc.
2109
2110 There are two ways to zonk a Type:
2111
2112 * zonkTcTypeToType, which is intended to be used at the end of type-checking
2113 for the final zonk. It has to deal with unfilled metavars, either by filling
2114 it with a value like Any or failing (determined by the UnboundTyVarZonker
2115 used).
2116
2117 * zonkTcType, which will happily ignore unfilled metavars. This is the
2118 appropriate function to use while in the middle of type-checking.
2119
2120 Note [Zonking to Skolem]
2121 ~~~~~~~~~~~~~~~~~~~~~~~~
2122 We used to zonk quantified type variables to regular TyVars. However, this
2123 leads to problems. Consider this program from the regression test suite:
2124
2125 eval :: Int -> String -> String -> String
2126 eval 0 root actual = evalRHS 0 root actual
2127
2128 evalRHS :: Int -> a
2129 evalRHS 0 root actual = eval 0 root actual
2130
2131 It leads to the deferral of an equality (wrapped in an implication constraint)
2132
2133 forall a. () => ((String -> String -> String) ~ a)
2134
2135 which is propagated up to the toplevel (see GHC.Tc.Solver.tcSimplifyInferCheck).
2136 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
2137 This has the *side effect* of also zonking the `a' in the deferred equality
2138 (which at this point is being handed around wrapped in an implication
2139 constraint).
2140
2141 Finally, the equality (with the zonked `a') will be handed back to the
2142 simplifier by GHC.Tc.Module.tcRnSrcDecls calling GHC.Tc.Solver.tcSimplifyTop.
2143 If we zonk `a' with a regular type variable, we will have this regular type
2144 variable now floating around in the simplifier, which in many places assumes to
2145 only see proper TcTyVars.
2146
2147 We can avoid this problem by zonking with a skolem TcTyVar. The
2148 skolem is rigid (which we require for a quantified variable), but is
2149 still a TcTyVar that the simplifier knows how to deal with.
2150
2151 Note [Skolemising and identity]
2152 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2153 In some places, we make a TyVarTv for a binder. E.g.
2154 class C a where ...
2155 As Note [Inferring kinds for type declarations] discusses,
2156 we make a TyVarTv for 'a'. Later we skolemise it, and we'd
2157 like to retain its identity, location info etc. (If we don't
2158 retain its identity we'll have to do some pointless swizzling;
2159 see GHC.Tc.TyCl.swizzleTcTyConBndrs. If we retain its identity
2160 but not its location we'll lose the detailed binding site info.
2161
2162 Conclusion: use the Name of the TyVarTv. But we don't want
2163 to do that when skolemising random unification variables;
2164 there the location we want is the skolemisation site.
2165
2166 Fortunately we can tell the difference: random unification
2167 variables have System Names. That's why final_name is
2168 set based on the isSystemName test.
2169
2170
2171 Note [Silly Type Synonyms]
2172 ~~~~~~~~~~~~~~~~~~~~~~~~~~
2173 Consider this:
2174 type C u a = u -- Note 'a' unused
2175
2176 foo :: (forall a. C u a -> C u a) -> u
2177 foo x = ...
2178
2179 bar :: Num u => u
2180 bar = foo (\t -> t + t)
2181
2182 * From the (\t -> t+t) we get type {Num d} => d -> d
2183 where d is fresh.
2184
2185 * Now unify with type of foo's arg, and we get:
2186 {Num (C d a)} => C d a -> C d a
2187 where a is fresh.
2188
2189 * Now abstract over the 'a', but float out the Num (C d a) constraint
2190 because it does not 'really' mention a. (see exactTyVarsOfType)
2191 The arg to foo becomes
2192 \/\a -> \t -> t+t
2193
2194 * So we get a dict binding for Num (C d a), which is zonked to give
2195 a = ()
2196 [Note Sept 04: now that we are zonking quantified type variables
2197 on construction, the 'a' will be frozen as a regular tyvar on
2198 quantification, so the floated dict will still have type (C d a).
2199 Which renders this whole note moot; happily!]
2200
2201 * Then the \/\a abstraction has a zonked 'a' in it.
2202
2203 All very silly. I think its harmless to ignore the problem. We'll end up with
2204 a \/\a in the final result but all the occurrences of a will be zonked to ()
2205 -}
2206
2207 {- *********************************************************************
2208 * *
2209 Promotion
2210 * *
2211 ********************************************************************* -}
2212
2213 promoteMetaTyVarTo :: TcLevel -> TcTyVar -> TcM Bool
2214 -- When we float a constraint out of an implication we must restore
2215 -- invariant (WantedInv) in Note [TcLevel invariants] in GHC.Tc.Utils.TcType
2216 -- Return True <=> we did some promotion
2217 -- Also returns either the original tyvar (no promotion) or the new one
2218 -- See Note [Promoting unification variables]
2219 promoteMetaTyVarTo tclvl tv
2220 | assertPpr (isMetaTyVar tv) (ppr tv) $
2221 tcTyVarLevel tv `strictlyDeeperThan` tclvl
2222 = do { cloned_tv <- cloneMetaTyVar tv
2223 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
2224 ; writeMetaTyVar tv (mkTyVarTy rhs_tv)
2225 ; traceTc "promoteTyVar" (ppr tv <+> text "-->" <+> ppr rhs_tv)
2226 ; return True }
2227 | otherwise
2228 = return False
2229
2230 -- Returns whether or not *any* tyvar is defaulted
2231 promoteTyVarSet :: TcTyVarSet -> TcM Bool
2232 promoteTyVarSet tvs
2233 = do { tclvl <- getTcLevel
2234 ; bools <- mapM (promoteMetaTyVarTo tclvl) $
2235 filter isPromotableMetaTyVar $
2236 nonDetEltsUniqSet tvs
2237 -- Non-determinism is OK because order of promotion doesn't matter
2238 ; return (or bools) }
2239
2240
2241 {- *********************************************************************
2242 * *
2243 Zonking types
2244 * *
2245 ********************************************************************* -}
2246
2247 zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
2248 -- Zonk a type and take its free variables
2249 -- With kind polymorphism it can be essential to zonk *first*
2250 -- so that we find the right set of free variables. Eg
2251 -- forall k1. forall (a:k2). a
2252 -- where k2:=k1 is in the substitution. We don't want
2253 -- k2 to look free in this type!
2254 zonkTcTypeAndFV ty
2255 = tyCoVarsOfTypeDSet <$> zonkTcType ty
2256
2257 zonkTyCoVar :: TyCoVar -> TcM TcType
2258 -- Works on TyVars and TcTyVars
2259 zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
2260 | isTyVar tv = mkTyVarTy <$> zonkTyCoVarKind tv
2261 | otherwise = assertPpr (isCoVar tv) (ppr tv) $
2262 mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
2263 -- Hackily, when typechecking type and class decls
2264 -- we have TyVars in scope added (only) in
2265 -- GHC.Tc.Gen.HsType.bindTyClTyVars, but it seems
2266 -- painful to make them into TcTyVars there
2267
2268 zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
2269 zonkTyCoVarsAndFV tycovars
2270 = tyCoVarsOfTypes <$> mapM zonkTyCoVar (nonDetEltsUniqSet tycovars)
2271 -- It's OK to use nonDetEltsUniqSet here because we immediately forget about
2272 -- the ordering by turning it into a nondeterministic set and the order
2273 -- of zonking doesn't matter for determinism.
2274
2275 zonkDTyCoVarSetAndFV :: DTyCoVarSet -> TcM DTyCoVarSet
2276 zonkDTyCoVarSetAndFV tycovars
2277 = mkDVarSet <$> (zonkTyCoVarsAndFVList $ dVarSetElems tycovars)
2278
2279 -- Takes a list of TyCoVars, zonks them and returns a
2280 -- deterministically ordered list of their free variables.
2281 zonkTyCoVarsAndFVList :: [TyCoVar] -> TcM [TyCoVar]
2282 zonkTyCoVarsAndFVList tycovars
2283 = tyCoVarsOfTypesList <$> mapM zonkTyCoVar tycovars
2284
2285 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
2286 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
2287
2288 ----------------- Types
2289 zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
2290 zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
2291 ; return (setTyVarKind tv kind') }
2292
2293 zonkTyCoVarKindBinder :: (VarBndr TyCoVar fl) -> TcM (VarBndr TyCoVar fl)
2294 zonkTyCoVarKindBinder (Bndr tv fl) = do { kind' <- zonkTcType (tyVarKind tv)
2295 ; return $ Bndr (setTyVarKind tv kind') fl }
2296
2297 {-
2298 ************************************************************************
2299 * *
2300 Zonking constraints
2301 * *
2302 ************************************************************************
2303 -}
2304
2305 zonkImplication :: Implication -> TcM Implication
2306 zonkImplication implic@(Implic { ic_skols = skols
2307 , ic_given = given
2308 , ic_wanted = wanted
2309 , ic_info = info })
2310 = do { skols' <- mapM zonkTyCoVarKind skols -- Need to zonk their kinds!
2311 -- as #7230 showed
2312 ; given' <- mapM zonkEvVar given
2313 ; info' <- zonkSkolemInfo info
2314 ; wanted' <- zonkWCRec wanted
2315 ; return (implic { ic_skols = skols'
2316 , ic_given = given'
2317 , ic_wanted = wanted'
2318 , ic_info = info' }) }
2319
2320 zonkEvVar :: EvVar -> TcM EvVar
2321 zonkEvVar var = updateIdTypeAndMultM zonkTcType var
2322
2323
2324 zonkWC :: WantedConstraints -> TcM WantedConstraints
2325 zonkWC wc = zonkWCRec wc
2326
2327 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
2328 zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_holes = holes })
2329 = do { simple' <- zonkSimples simple
2330 ; implic' <- mapBagM zonkImplication implic
2331 ; holes' <- mapBagM zonkHole holes
2332 ; return (WC { wc_simple = simple', wc_impl = implic', wc_holes = holes' }) }
2333
2334 zonkSimples :: Cts -> TcM Cts
2335 zonkSimples cts = do { cts' <- mapBagM zonkCt cts
2336 ; traceTc "zonkSimples done:" (ppr cts')
2337 ; return cts' }
2338
2339 zonkHole :: Hole -> TcM Hole
2340 zonkHole hole@(Hole { hole_ty = ty })
2341 = do { ty' <- zonkTcType ty
2342 ; return (hole { hole_ty = ty' }) }
2343
2344 {- Note [zonkCt behaviour]
2345 ~~~~~~~~~~~~~~~~~~~~~~~~~~
2346 zonkCt tries to maintain the canonical form of a Ct. For example,
2347 - a CDictCan should stay a CDictCan;
2348 - a CIrredCan should stay a CIrredCan with its cc_reason flag intact
2349
2350 Why?, for example:
2351 - For CDictCan, the @GHC.Tc.Solver.expandSuperClasses@ step, which runs after the
2352 simple wanted and plugin loop, looks for @CDictCan@s. If a plugin is in use,
2353 constraints are zonked before being passed to the plugin. This means if we
2354 don't preserve a canonical form, @expandSuperClasses@ fails to expand
2355 superclasses. This is what happened in #11525.
2356
2357 - For CIrredCan we want to see if a constraint is insoluble with insolubleWC
2358
2359 On the other hand, we change CEqCan to CNonCanonical, because of all of
2360 CEqCan's invariants, which can break during zonking. (Example: a ~R alpha, where
2361 we have alpha := N Int, where N is a newtype.) Besides, the constraint
2362 will be canonicalised again, so there is little benefit in keeping the
2363 CEqCan structure.
2364
2365 NB: Constraints are always rewritten etc by the canonicaliser in
2366 @GHC.Tc.Solver.Canonical@ even if they come in as CDictCan. Only canonical constraints that
2367 are actually in the inert set carry all the guarantees. So it is okay if zonkCt
2368 creates e.g. a CDictCan where the cc_tyars are /not/ fully reduced.
2369 -}
2370
2371 zonkCt :: Ct -> TcM Ct
2372 -- See Note [zonkCt behaviour]
2373 zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
2374 = do { ev' <- zonkCtEvidence ev
2375 ; args' <- mapM zonkTcType args
2376 ; return $ ct { cc_ev = ev', cc_tyargs = args' } }
2377
2378 zonkCt (CEqCan { cc_ev = ev })
2379 = mkNonCanonical <$> zonkCtEvidence ev
2380
2381 zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_reason flag
2382 = do { ev' <- zonkCtEvidence ev
2383 ; return (ct { cc_ev = ev' }) }
2384
2385 zonkCt ct
2386 = do { fl' <- zonkCtEvidence (ctEvidence ct)
2387 ; return (mkNonCanonical fl') }
2388
2389 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
2390 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
2391 = do { pred' <- zonkTcType pred
2392 ; return (ctev { ctev_pred = pred'}) }
2393 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest })
2394 = do { pred' <- zonkTcType pred
2395 ; let dest' = case dest of
2396 EvVarDest ev -> EvVarDest $ setVarType ev pred'
2397 -- necessary in simplifyInfer
2398 HoleDest h -> HoleDest h
2399 ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
2400 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
2401 = do { pred' <- zonkTcType pred
2402 ; return (ctev { ctev_pred = pred' }) }
2403
2404 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
2405 zonkSkolemInfo (SigSkol cx ty tv_prs) = do { ty' <- zonkTcType ty
2406 ; return (SigSkol cx ty' tv_prs) }
2407 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
2408 ; return (InferSkol ntys') }
2409 where
2410 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
2411 zonkSkolemInfo skol_info = return skol_info
2412
2413 {-
2414 %************************************************************************
2415 %* *
2416 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
2417 * *
2418 * For internal use only! *
2419 * *
2420 ************************************************************************
2421
2422 -}
2423
2424 -- For unbound, mutable tyvars, zonkType uses the function given to it
2425 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
2426 -- type variable and zonks the kind too
2427 zonkTcType :: TcType -> TcM TcType
2428 zonkTcTypes :: [TcType] -> TcM [TcType]
2429 zonkCo :: Coercion -> TcM Coercion
2430
2431 (zonkTcType, zonkTcTypes, zonkCo, _)
2432 = mapTyCo zonkTcTypeMapper
2433
2434 -- | A suitable TyCoMapper for zonking a type during type-checking,
2435 -- before all metavars are filled in.
2436 zonkTcTypeMapper :: TyCoMapper () TcM
2437 zonkTcTypeMapper = TyCoMapper
2438 { tcm_tyvar = const zonkTcTyVar
2439 , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
2440 , tcm_hole = hole
2441 , tcm_tycobinder = \_env tv _vis -> ((), ) <$> zonkTyCoVarKind tv
2442 , tcm_tycon = zonkTcTyCon }
2443 where
2444 hole :: () -> CoercionHole -> TcM Coercion
2445 hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
2446 = do { contents <- readTcRef ref
2447 ; case contents of
2448 Just co -> do { co' <- zonkCo co
2449 ; checkCoercionHole cv co' }
2450 Nothing -> do { cv' <- zonkCoVar cv
2451 ; return $ HoleCo (hole { ch_co_var = cv' }) } }
2452
2453 zonkTcTyCon :: TcTyCon -> TcM TcTyCon
2454 -- Only called on TcTyCons
2455 -- A non-poly TcTyCon may have unification
2456 -- variables that need zonking, but poly ones cannot
2457 zonkTcTyCon tc
2458 | tcTyConIsPoly tc = return tc
2459 | otherwise = do { tck' <- zonkTcType (tyConKind tc)
2460 ; return (setTcTyConKind tc tck') }
2461
2462 zonkTcTyVar :: TcTyVar -> TcM TcType
2463 -- Simply look through all Flexis
2464 zonkTcTyVar tv
2465 | isTcTyVar tv
2466 = case tcTyVarDetails tv of
2467 SkolemTv {} -> zonk_kind_and_return
2468 RuntimeUnk {} -> zonk_kind_and_return
2469 MetaTv { mtv_ref = ref }
2470 -> do { cts <- readMutVar ref
2471 ; case cts of
2472 Flexi -> zonk_kind_and_return
2473 Indirect ty -> do { zty <- zonkTcType ty
2474 ; writeTcRef ref (Indirect zty)
2475 -- See Note [Sharing in zonking]
2476 ; return zty } }
2477
2478 | otherwise -- coercion variable
2479 = zonk_kind_and_return
2480 where
2481 zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv
2482 ; return (mkTyVarTy z_tv) }
2483
2484 -- Variant that assumes that any result of zonking is still a TyVar.
2485 -- Should be used only on skolems and TyVarTvs
2486 zonkTcTyVarToTyVar :: HasDebugCallStack => TcTyVar -> TcM TcTyVar
2487 zonkTcTyVarToTyVar tv
2488 = do { ty <- zonkTcTyVar tv
2489 ; let tv' = case tcGetTyVar_maybe ty of
2490 Just tv' -> tv'
2491 Nothing -> pprPanic "zonkTcTyVarToTyVar"
2492 (ppr tv $$ ppr ty)
2493 ; return tv' }
2494
2495 zonkInvisTVBinder :: VarBndr TcTyVar spec -> TcM (VarBndr TyVar spec)
2496 zonkInvisTVBinder (Bndr tv spec) = do { tv' <- zonkTcTyVarToTyVar tv
2497 ; return (Bndr tv' spec) }
2498
2499 -- zonkId is used *during* typechecking just to zonk the Id's type
2500 zonkId :: TcId -> TcM TcId
2501 zonkId id = Id.updateIdTypeAndMultM zonkTcType id
2502
2503 zonkCoVar :: CoVar -> TcM CoVar
2504 zonkCoVar = zonkId
2505
2506 {- Note [Sharing in zonking]
2507 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2508 Suppose we have
2509 alpha :-> beta :-> gamma :-> ty
2510 where the ":->" means that the unification variable has been
2511 filled in with Indirect. Then when zonking alpha, it'd be nice
2512 to short-circuit beta too, so we end up with
2513 alpha :-> zty
2514 beta :-> zty
2515 gamma :-> zty
2516 where zty is the zonked version of ty. That way, if we come across
2517 beta later, we'll have less work to do. (And indeed the same for
2518 alpha.)
2519
2520 This is easily achieved: just overwrite (Indirect ty) with (Indirect
2521 zty). Non-systematic perf comparisons suggest that this is a modest
2522 win.
2523
2524 But c.f Note [Sharing when zonking to Type] in GHC.Tc.Utils.Zonk.
2525
2526 %************************************************************************
2527 %* *
2528 Tidying
2529 * *
2530 ************************************************************************
2531 -}
2532
2533 zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
2534 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
2535 ; return (tidyOpenType env ty') }
2536
2537 zonkTidyTcTypes :: TidyEnv -> [TcType] -> TcM (TidyEnv, [TcType])
2538 zonkTidyTcTypes = zonkTidyTcTypes' []
2539 where zonkTidyTcTypes' zs env [] = return (env, reverse zs)
2540 zonkTidyTcTypes' zs env (ty:tys)
2541 = do { (env', ty') <- zonkTidyTcType env ty
2542 ; zonkTidyTcTypes' (ty':zs) env' tys }
2543
2544 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
2545 zonkTidyOrigin env (GivenOrigin skol_info)
2546 = do { skol_info1 <- zonkSkolemInfo skol_info
2547 ; let skol_info2 = tidySkolemInfo env skol_info1
2548 ; return (env, GivenOrigin skol_info2) }
2549 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act
2550 , uo_expected = exp })
2551 = do { (env1, act') <- zonkTidyTcType env act
2552 ; (env2, exp') <- zonkTidyTcType env1 exp
2553 ; return ( env2, orig { uo_actual = act'
2554 , uo_expected = exp' }) }
2555 zonkTidyOrigin env (KindEqOrigin ty1 ty2 orig t_or_k)
2556 = do { (env1, ty1') <- zonkTidyTcType env ty1
2557 ; (env2, ty2') <- zonkTidyTcType env1 ty2
2558 ; (env3, orig') <- zonkTidyOrigin env2 orig
2559 ; return (env3, KindEqOrigin ty1' ty2' orig' t_or_k) }
2560 zonkTidyOrigin env (FunDepOrigin1 p1 o1 l1 p2 o2 l2)
2561 = do { (env1, p1') <- zonkTidyTcType env p1
2562 ; (env2, p2') <- zonkTidyTcType env1 p2
2563 ; return (env2, FunDepOrigin1 p1' o1 l1 p2' o2 l2) }
2564 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
2565 = do { (env1, p1') <- zonkTidyTcType env p1
2566 ; (env2, p2') <- zonkTidyTcType env1 p2
2567 ; (env3, o1') <- zonkTidyOrigin env2 o1
2568 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
2569 zonkTidyOrigin env (CycleBreakerOrigin orig)
2570 = do { (env1, orig') <- zonkTidyOrigin env orig
2571 ; return (env1, CycleBreakerOrigin orig') }
2572 zonkTidyOrigin env (InstProvidedOrigin mod cls_inst)
2573 = do { (env1, is_tys') <- mapAccumLM zonkTidyTcType env (is_tys cls_inst)
2574 ; return (env1, InstProvidedOrigin mod (cls_inst {is_tys = is_tys'})) }
2575 zonkTidyOrigin env (FixedRuntimeRepOrigin ty frr_orig)
2576 = do { (env1, ty') <- zonkTidyTcType env ty
2577 ; return (env1, FixedRuntimeRepOrigin ty' frr_orig)}
2578 zonkTidyOrigin env orig = return (env, orig)
2579
2580 zonkTidyOrigins :: TidyEnv -> [CtOrigin] -> TcM (TidyEnv, [CtOrigin])
2581 zonkTidyOrigins = mapAccumLM zonkTidyOrigin
2582
2583 ----------------
2584 tidyCt :: TidyEnv -> Ct -> Ct
2585 -- Used only in error reporting
2586 tidyCt env ct
2587 = ct { cc_ev = tidy_ev (ctEvidence ct) }
2588 where
2589 tidy_ev :: CtEvidence -> CtEvidence
2590 -- NB: we do not tidy the ctev_evar field because we don't
2591 -- show it in error messages
2592 tidy_ev ctev = ctev { ctev_pred = tidyType env (ctev_pred ctev) }
2593
2594 tidyHole :: TidyEnv -> Hole -> Hole
2595 tidyHole env h@(Hole { hole_ty = ty }) = h { hole_ty = tidyType env ty }
2596
2597 ----------------
2598 tidyEvVar :: TidyEnv -> EvVar -> EvVar
2599 tidyEvVar env var = updateIdTypeAndMult (tidyType env) var
2600
2601 ----------------
2602 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
2603 tidySkolemInfo env (DerivSkol ty) = DerivSkol (tidyType env ty)
2604 tidySkolemInfo env (SigSkol cx ty tv_prs) = tidySigSkol env cx ty tv_prs
2605 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
2606 tidySkolemInfo env (UnifyForAllSkol ty) = UnifyForAllSkol (tidyType env ty)
2607 tidySkolemInfo _ info = info
2608
2609 tidySigSkol :: TidyEnv -> UserTypeCtxt
2610 -> TcType -> [(Name,TcTyVar)] -> SkolemInfo
2611 -- We need to take special care when tidying SigSkol
2612 -- See Note [SigSkol SkolemInfo] in "GHC.Tc.Types.Origin"
2613 tidySigSkol env cx ty tv_prs
2614 = SigSkol cx (tidy_ty env ty) tv_prs'
2615 where
2616 tv_prs' = mapSnd (tidyTyCoVarOcc env) tv_prs
2617 inst_env = mkNameEnv tv_prs'
2618
2619 tidy_ty env (ForAllTy (Bndr tv vis) ty)
2620 = ForAllTy (Bndr tv' vis) (tidy_ty env' ty)
2621 where
2622 (env', tv') = tidy_tv_bndr env tv
2623
2624 tidy_ty env ty@(FunTy InvisArg w arg res) -- Look under c => t
2625 = ty { ft_mult = tidy_ty env w,
2626 ft_arg = tidyType env arg,
2627 ft_res = tidy_ty env res }
2628
2629 tidy_ty env ty = tidyType env ty
2630
2631 tidy_tv_bndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
2632 tidy_tv_bndr env@(occ_env, subst) tv
2633 | Just tv' <- lookupNameEnv inst_env (tyVarName tv)
2634 = ((occ_env, extendVarEnv subst tv tv'), tv')
2635
2636 | otherwise
2637 = tidyVarBndr env tv
2638
2639 -------------------------------------------------------------------------
2640 {-
2641 %************************************************************************
2642 %* *
2643 Representation polymorphism checks
2644 * *
2645 ***********************************************************************-}
2646
2647 -- | Check that the specified type has a fixed runtime representation.
2648 --
2649 -- If it isn't, throw a representation-polymorphism error appropriate
2650 -- for the context (as specified by the 'FixedRuntimeRepProvenance').
2651 --
2652 -- Unlike the other representation polymorphism checks, which emit
2653 -- 'Concrete#' constraints, this function does not emit any constraints,
2654 -- as it has enough information to immediately make a decision.
2655 --
2656 -- See (1) in Note [Representation polymorphism checking] in GHC.Tc.Utils.Concrete
2657 checkTypeHasFixedRuntimeRep :: FixedRuntimeRepProvenance -> Type -> TcM ()
2658 checkTypeHasFixedRuntimeRep prov ty =
2659 unless (typeHasFixedRuntimeRep ty)
2660 (addDetailedDiagnostic $ TcRnTypeDoesNotHaveFixedRuntimeRep ty prov)
2661
2662 {-
2663 %************************************************************************
2664 %* *
2665 Error messages
2666 * *
2667 *************************************************************************
2668
2669 -}
2670
2671 -- See Note [Naughty quantification candidates]
2672 naughtyQuantification :: TcType -- original type user wanted to quantify
2673 -> TcTyVar -- naughty var
2674 -> TyVarSet -- skolems that would escape
2675 -> TcM a
2676 naughtyQuantification orig_ty tv escapees
2677 = do { orig_ty1 <- zonkTcType orig_ty -- in case it's not zonked
2678
2679 ; escapees' <- mapM zonkTcTyVarToTyVar $
2680 nonDetEltsUniqSet escapees
2681 -- we'll just be printing, so no harmful non-determinism
2682
2683 ; let fvs = tyCoVarsOfTypeWellScoped orig_ty1
2684 env0 = tidyFreeTyCoVars emptyTidyEnv fvs
2685 env = env0 `delTidyEnvList` escapees'
2686 -- this avoids gratuitous renaming of the escaped
2687 -- variables; very confusing to users!
2688
2689 orig_ty' = tidyType env orig_ty1
2690 ppr_tidied = pprTyVars . map (tidyTyCoVarOcc env)
2691 msg = TcRnUnknownMessage $ mkPlainError noHints $
2692 pprWithExplicitKindsWhen True $
2693 vcat [ sep [ text "Cannot generalise type; skolem" <> plural escapees'
2694 , quotes $ ppr_tidied escapees'
2695 , text "would escape" <+> itsOrTheir escapees' <+> text "scope"
2696 ]
2697 , sep [ text "if I tried to quantify"
2698 , ppr_tidied [tv]
2699 , text "in this type:"
2700 ]
2701 , nest 2 (pprTidiedType orig_ty')
2702 , text "(Indeed, I sometimes struggle even printing this correctly,"
2703 , text " due to its ill-scoped nature.)"
2704 ]
2705
2706 ; failWithTcM (env, msg) }