Fix #11334.
[ghc.git] / compiler / typecheck / TcMType.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5
6 Monadic type operations
7
8 This module contains monadic operations over types that contain
9 mutable type variables
10 -}
11
12 {-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
13
14 module TcMType (
15 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
16
17 --------------------------------
18 -- Creating new mutable type variables
19 newFlexiTyVar,
20 newFlexiTyVarTy, -- Kind -> TcM TcType
21 newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
22 newOpenFlexiTyVarTy,
23 newMetaKindVar, newMetaKindVars,
24 cloneMetaTyVar,
25 newFmvTyVar, newFskTyVar,
26
27 readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
28 newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
29
30 --------------------------------
31 -- Expected types
32 ExpType(..), ExpSigmaType, ExpRhoType,
33 mkCheckExpType, newOpenInferExpType, readExpType, readExpType_maybe,
34 writeExpType, expTypeToType, checkingExpType_maybe, checkingExpType,
35 tauifyExpType,
36
37 --------------------------------
38 -- Creating fresh type variables for pm checking
39 genInstSkolTyVarsX,
40
41 --------------------------------
42 -- Creating new evidence variables
43 newEvVar, newEvVars, newDict,
44 newWanted, newWanteds,
45 emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
46 newTcEvBinds, addTcEvBind,
47
48 newCoercionHole, fillCoercionHole, isFilledCoercionHole,
49 unpackCoercionHole, unpackCoercionHole_maybe,
50 checkCoercionHole,
51
52 --------------------------------
53 -- Instantiation
54 newMetaTyVars, newMetaTyVarX, newMetaSigTyVars,
55 newSigTyVar,
56 tcInstType,
57 tcInstSkolTyVars, tcInstSkolTyVarsLoc, tcInstSuperSkolTyVarsX,
58 tcInstSigTyVarsLoc, tcInstSigTyVars,
59 tcInstSkolType,
60 tcSkolDFunType, tcSuperSkolTyVars,
61
62 instSkolTyCoVars, freshenTyVarBndrs, freshenCoVarBndrsX,
63
64 --------------------------------
65 -- Zonking and tidying
66 zonkTidyTcType, zonkTidyOrigin,
67 mkTypeErrorThing, mkTypeErrorThingArgs,
68 tidyEvVar, tidyCt, tidySkolemInfo,
69 skolemiseUnboundMetaTyVar,
70 zonkTcTyVar, zonkTcTyVars, zonkTyCoVarsAndFV, zonkTcTypeAndFV,
71 zonkQuantifiedTyVar, zonkQuantifiedTyVarOrType, quantifyTyVars,
72 defaultKindVar,
73 zonkTcTyCoVarBndr, zonkTcTyBinder, zonkTcType, zonkTcTypes, zonkCo,
74 zonkTyCoVarKind, zonkTcTypeMapper,
75
76 zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo,
77
78 tcGetGlobalTyCoVars
79 ) where
80
81 #include "HsVersions.h"
82
83 -- friends:
84 import TyCoRep
85 import TcType
86 import Type
87 import Kind
88 import Coercion
89 import Class
90 import Var
91
92 -- others:
93 import TcRnMonad -- TcType, amongst others
94 import TcEvidence
95 import Id
96 import Name
97 import VarSet
98 import TysWiredIn
99 import TysPrim
100 import VarEnv
101 import PrelNames
102 import Util
103 import Outputable
104 import FastString
105 import SrcLoc
106 import Bag
107 import Pair
108 import qualified GHC.LanguageExtensions as LangExt
109
110 import Control.Monad
111 import Maybes
112 import Data.List ( mapAccumL, partition )
113 import Control.Arrow ( second )
114
115 {-
116 ************************************************************************
117 * *
118 Kind variables
119 * *
120 ************************************************************************
121 -}
122
123 mkKindName :: Unique -> Name
124 mkKindName unique = mkSystemName unique kind_var_occ
125
126 kind_var_occ :: OccName -- Just one for all MetaKindVars
127 -- They may be jiggled by tidying
128 kind_var_occ = mkOccName tvName "k"
129
130 newMetaKindVar :: TcM TcKind
131 newMetaKindVar = do { uniq <- newUnique
132 ; details <- newMetaDetails TauTv
133 ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
134 ; return (mkTyVarTy kv) }
135
136 newMetaKindVars :: Int -> TcM [TcKind]
137 newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
138
139 {-
140 ************************************************************************
141 * *
142 Evidence variables; range over constraints we can abstract over
143 * *
144 ************************************************************************
145 -}
146
147 newEvVars :: TcThetaType -> TcM [EvVar]
148 newEvVars theta = mapM newEvVar theta
149
150 --------------
151
152 newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar
153 -- Creates new *rigid* variables for predicates
154 newEvVar ty = do { name <- newSysName (predTypeOccName ty)
155 ; return (mkLocalIdOrCoVar name ty) }
156
157 newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
158 -- Deals with both equality and non-equality predicates
159 newWanted orig t_or_k pty
160 = do loc <- getCtLocM orig t_or_k
161 d <- if isEqPred pty then HoleDest <$> newCoercionHole
162 else EvVarDest <$> newEvVar pty
163 return $ CtWanted { ctev_dest = d
164 , ctev_pred = pty
165 , ctev_loc = loc }
166
167 newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
168 newWanteds orig = mapM (newWanted orig Nothing)
169
170 -- | Emits a new Wanted. Deals with both equalities and non-equalities.
171 emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
172 emitWanted origin pty
173 = do { ev <- newWanted origin Nothing pty
174 ; emitSimple $ mkNonCanonical ev
175 ; return $ ctEvTerm ev }
176
177 -- | Emits a new equality constraint
178 emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
179 emitWantedEq origin t_or_k role ty1 ty2
180 = do { hole <- newCoercionHole
181 ; loc <- getCtLocM origin (Just t_or_k)
182 ; emitSimple $ mkNonCanonical $
183 CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole, ctev_loc = loc }
184 ; return (mkHoleCo hole role ty1 ty2) }
185 where
186 pty = mkPrimEqPredRole role ty1 ty2
187
188 -- | Creates a new EvVar and immediately emits it as a Wanted.
189 -- No equality predicates here.
190 emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
191 emitWantedEvVar origin ty
192 = do { new_cv <- newEvVar ty
193 ; loc <- getCtLocM origin Nothing
194 ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
195 , ctev_pred = ty
196 , ctev_loc = loc }
197 ; emitSimple $ mkNonCanonical ctev
198 ; return new_cv }
199
200 emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
201 emitWantedEvVars orig = mapM (emitWantedEvVar orig)
202
203 newDict :: Class -> [TcType] -> TcM DictId
204 newDict cls tys
205 = do { name <- newSysName (mkDictOcc (getOccName cls))
206 ; return (mkLocalId name (mkClassPred cls tys)) }
207
208 predTypeOccName :: PredType -> OccName
209 predTypeOccName ty = case classifyPredType ty of
210 ClassPred cls _ -> mkDictOcc (getOccName cls)
211 EqPred _ _ _ -> mkVarOccFS (fsLit "cobox")
212 IrredPred _ -> mkVarOccFS (fsLit "irred")
213
214 {-
215 ************************************************************************
216 * *
217 Coercion holes
218 * *
219 ************************************************************************
220 -}
221
222 newCoercionHole :: TcM CoercionHole
223 newCoercionHole
224 = do { u <- newUnique
225 ; traceTc "New coercion hole:" (ppr u)
226 ; ref <- newMutVar Nothing
227 ; return $ CoercionHole u ref }
228
229 -- | Put a value in a coercion hole
230 fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
231 fillCoercionHole (CoercionHole u ref) co
232 = do {
233 #ifdef DEBUG
234 ; cts <- readTcRef ref
235 ; whenIsJust cts $ \old_co ->
236 pprPanic "Filling a filled coercion hole" (ppr u $$ ppr co $$ ppr old_co)
237 #endif
238 ; traceTc "Filling coercion hole" (ppr u <+> text ":=" <+> ppr co)
239 ; writeTcRef ref (Just co) }
240
241 -- | Is a coercion hole filled in?
242 isFilledCoercionHole :: CoercionHole -> TcM Bool
243 isFilledCoercionHole (CoercionHole _ ref) = isJust <$> readTcRef ref
244
245 -- | Retrieve the contents of a coercion hole. Panics if the hole
246 -- is unfilled
247 unpackCoercionHole :: CoercionHole -> TcM Coercion
248 unpackCoercionHole hole
249 = do { contents <- unpackCoercionHole_maybe hole
250 ; case contents of
251 Just co -> return co
252 Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) }
253
254 -- | Retrieve the contents of a coercion hole, if it is filled
255 unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
256 unpackCoercionHole_maybe (CoercionHole _ ref) = readTcRef ref
257
258 -- | Check that a coercion is appropriate for filling a hole. (The hole
259 -- itself is needed only for printing. NB: This must be /lazy/ in the coercion,
260 -- as it's used in TcHsSyn in the presence of knots.
261 -- Always returns the checked coercion, but this return value is necessary
262 -- so that the input coercion is forced only when the output is forced.
263 checkCoercionHole :: Coercion -> CoercionHole -> Role -> Type -> Type -> TcM Coercion
264 checkCoercionHole co h r t1 t2
265 -- co is already zonked, but t1 and t2 might not be
266 | debugIsOn
267 = do { t1 <- zonkTcType t1
268 ; t2 <- zonkTcType t2
269 ; let (Pair _t1 _t2, _role) = coercionKindRole co
270 ; return $
271 ASSERT2( t1 `eqType` _t1 && t2 `eqType` _t2 && r == _role
272 , (text "Bad coercion hole" <+>
273 ppr h <> colon <+> vcat [ ppr _t1, ppr _t2, ppr _role
274 , ppr co, ppr t1, ppr t2
275 , ppr r ]) )
276 co }
277 | otherwise
278 = return co
279
280 {-
281 ************************************************************************
282 *
283 Expected types
284 *
285 ************************************************************************
286
287 Note [ExpType]
288 ~~~~~~~~~~~~~~
289
290 An ExpType is used as the "expected type" when type-checking an expression.
291 An ExpType can hold a "hole" that can be filled in by the type-checker.
292 This allows us to have one tcExpr that works in both checking mode and
293 synthesis mode (that is, bidirectional type-checking). Previously, this
294 was achieved by using ordinary unification variables, but we don't need
295 or want that generality. (For example, #11397 was caused by doing the
296 wrong thing with unification variables.) Instead, we observe that these
297 holes should
298
299 1. never be nested
300 2. never appear as the type of a variable
301 3. be used linearly (never be duplicated)
302
303 By defining ExpType, separately from Type, we can achieve goals 1 and 2
304 statically.
305
306 See also [wiki:Typechecking]
307
308 Note [TcLevel of ExpType]
309 ~~~~~~~~~~~~~~~~~~~~~~~~~
310 Consider
311
312 data G a where
313 MkG :: G Bool
314
315 foo MkG = True
316
317 This is a classic untouchable-variable / ambiguous GADT return type
318 scenario. But, with ExpTypes, we'll be inferring the type of the RHS.
319 And, because there is only one branch of the case, we won't trigger
320 Note [Case branches must never infer a non-tau type] of TcMatches.
321 We thus must track a TcLevel in an Inferring ExpType. If we try to
322 fill the ExpType and find that the TcLevels don't work out, we
323 fill the ExpType with a tau-tv at the low TcLevel, hopefully to
324 be worked out later by some means. This is triggered in
325 test gadt/gadt-escape1.
326
327 -}
328
329 -- actual data definition is in TcType
330
331 -- | Make an 'ExpType' suitable for inferring a type of kind * or #.
332 newOpenInferExpType :: TcM ExpType
333 newOpenInferExpType
334 = do { rr <- newFlexiTyVarTy runtimeRepTy
335 ; u <- newUnique
336 ; tclvl <- getTcLevel
337 ; let ki = tYPE rr
338 ; traceTc "newOpenInferExpType" (ppr u <+> dcolon <+> ppr ki)
339 ; ref <- newMutVar Nothing
340 ; return (Infer u tclvl ki ref) }
341
342 -- | Extract a type out of an ExpType, if one exists. But one should always
343 -- exist. Unless you're quite sure you know what you're doing.
344 readExpType_maybe :: ExpType -> TcM (Maybe TcType)
345 readExpType_maybe (Check ty) = return (Just ty)
346 readExpType_maybe (Infer _ _ _ ref) = readMutVar ref
347
348 -- | Extract a type out of an ExpType. Otherwise, panics.
349 readExpType :: ExpType -> TcM TcType
350 readExpType exp_ty
351 = do { mb_ty <- readExpType_maybe exp_ty
352 ; case mb_ty of
353 Just ty -> return ty
354 Nothing -> pprPanic "Unknown expected type" (ppr exp_ty) }
355
356 -- | Write into an 'ExpType'. It must be an 'Infer'.
357 writeExpType :: ExpType -> TcType -> TcM ()
358 writeExpType (Infer u tc_lvl ki ref) ty
359 | debugIsOn
360 = do { ki1 <- zonkTcType (typeKind ty)
361 ; ki2 <- zonkTcType ki
362 ; MASSERT2( ki1 `eqType` ki2, ppr ki1 $$ ppr ki2 $$ ppr u )
363 ; lvl_now <- getTcLevel
364 ; MASSERT2( tc_lvl == lvl_now, ppr u $$ ppr tc_lvl $$ ppr lvl_now )
365 ; cts <- readTcRef ref
366 ; case cts of
367 Just already_there -> pprPanic "writeExpType"
368 (vcat [ ppr u
369 , ppr ty
370 , ppr already_there ])
371 Nothing -> write }
372 | otherwise
373 = write
374 where
375 write = do { traceTc "Filling ExpType" $
376 ppr u <+> text ":=" <+> ppr ty
377 ; writeTcRef ref (Just ty) }
378 writeExpType (Check ty1) ty2 = pprPanic "writeExpType" (ppr ty1 $$ ppr ty2)
379
380 -- | Returns the expected type when in checking mode.
381 checkingExpType_maybe :: ExpType -> Maybe TcType
382 checkingExpType_maybe (Check ty) = Just ty
383 checkingExpType_maybe _ = Nothing
384
385 -- | Returns the expected type when in checking mode. Panics if in inference
386 -- mode.
387 checkingExpType :: String -> ExpType -> TcType
388 checkingExpType _ (Check ty) = ty
389 checkingExpType err et = pprPanic "checkingExpType" (text err $$ ppr et)
390
391 tauifyExpType :: ExpType -> TcM ExpType
392 -- ^ Turn a (Infer hole) type into a (Check alpha),
393 -- where alpha is a fresh unificaiton variable
394 tauifyExpType exp_ty = do { ty <- expTypeToType exp_ty
395 ; return (Check ty) }
396
397 -- | Extracts the expected type if there is one, or generates a new
398 -- TauTv if there isn't.
399 expTypeToType :: ExpType -> TcM TcType
400 expTypeToType (Check ty) = return ty
401 expTypeToType (Infer u tc_lvl ki ref)
402 = do { uniq <- newUnique
403 ; tv_ref <- newMutVar Flexi
404 ; let details = MetaTv { mtv_info = TauTv
405 , mtv_ref = tv_ref
406 , mtv_tclvl = tc_lvl }
407 name = mkMetaTyVarName uniq (fsLit "t")
408 tau_tv = mkTcTyVar name ki details
409 tau = mkTyVarTy tau_tv
410 -- can't use newFlexiTyVarTy because we need to set the tc_lvl
411 -- See also Note [TcLevel of ExpType]
412
413 ; writeMutVar ref (Just tau)
414 ; traceTc "Forcing ExpType to be monomorphic:"
415 (ppr u <+> dcolon <+> ppr ki <+> text ":=" <+> ppr tau)
416 ; return tau }
417
418 {-
419 ************************************************************************
420 * *
421 SkolemTvs (immutable)
422 * *
423 ************************************************************************
424 -}
425
426 tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
427 -- ^ How to instantiate the type variables
428 -> TcType -- ^ Type to instantiate
429 -> TcM ([TcTyVar], TcThetaType, TcType) -- ^ Result
430 -- (type vars, preds (incl equalities), rho)
431 tcInstType inst_tyvars ty
432 = case tcSplitForAllTys ty of
433 ([], rho) -> let -- There may be overloading despite no type variables;
434 -- (?x :: Int) => Int -> Int
435 (theta, tau) = tcSplitPhiTy rho
436 in
437 return ([], theta, tau)
438
439 (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
440 ; let (theta, tau) = tcSplitPhiTy (substTyUnchecked subst rho)
441 ; return (tyvars', theta, tau) }
442
443 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
444 -- Instantiate a type signature with skolem constants.
445 -- We could give them fresh names, but no need to do so
446 tcSkolDFunType ty = tcInstType tcInstSuperSkolTyVars ty
447
448 tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
449 -- Make skolem constants, but do *not* give them new names, as above
450 -- Moreover, make them "super skolems"; see comments with superSkolemTv
451 -- see Note [Kind substitution when instantiating]
452 -- Precondition: tyvars should be ordered by scoping
453 tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
454
455 tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
456 tcSuperSkolTyVar subst tv
457 = (extendTvSubstWithClone subst tv new_tv, new_tv)
458 where
459 kind = substTyUnchecked subst (tyVarKind tv)
460 new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
461
462 -- Wrappers
463 -- we need to be able to do this from outside the TcM monad:
464 tcInstSkolTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
465 tcInstSkolTyVarsLoc loc = instSkolTyCoVars (mkTcSkolTyVar loc False)
466
467 tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
468 tcInstSkolTyVars = tcInstSkolTyVars' False emptyTCvSubst
469
470 tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
471 tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
472
473 tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
474 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
475
476 tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
477 -- Precondition: tyvars should be ordered (kind vars first)
478 -- see Note [Kind substitution when instantiating]
479 -- Get the location from the monad; this is a complete freshening operation
480 tcInstSkolTyVars' overlappable subst tvs
481 = do { loc <- getSrcSpanM
482 ; instSkolTyCoVarsX (mkTcSkolTyVar loc overlappable) subst tvs }
483
484 mkTcSkolTyVar :: SrcSpan -> Bool -> Unique -> Name -> Kind -> TcTyVar
485 mkTcSkolTyVar loc overlappable uniq old_name kind
486 = mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
487 kind
488 (SkolemTv overlappable)
489
490 tcInstSigTyVarsLoc :: SrcSpan -> [TyVar]
491 -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
492 -- We specify the location
493 tcInstSigTyVarsLoc loc = instSkolTyCoVars (mkTcSkolTyVar loc False)
494
495 tcInstSigTyVars :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
496 -- Get the location from the TyVar itself, not the monad
497 tcInstSigTyVars
498 = instSkolTyCoVars mk_tv
499 where
500 mk_tv uniq old_name kind
501 = mkTcTyVar (setNameUnique old_name uniq) kind (SkolemTv False)
502
503 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
504 -- Instantiate a type with fresh skolem constants
505 -- Binding location comes from the monad
506 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
507
508 ------------------
509 freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
510 -- ^ Give fresh uniques to a bunch of TyVars, but they stay
511 -- as TyVars, rather than becoming TcTyVars
512 -- Used in FamInst.newFamInst, and Inst.newClsInst
513 freshenTyVarBndrs = instSkolTyCoVars mk_tv
514 where
515 mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
516
517 freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcRnIf gbl lcl (TCvSubst, [CoVar])
518 -- ^ Give fresh uniques to a bunch of CoVars
519 -- Used in FamInst.newFamInst
520 freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
521 where
522 mk_cv uniq old_name kind = mkCoVar (setNameUnique old_name uniq) kind
523
524 ------------------
525 instSkolTyCoVars :: (Unique -> Name -> Kind -> TyCoVar)
526 -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
527 instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
528
529 instSkolTyCoVarsX :: (Unique -> Name -> Kind -> TyCoVar)
530 -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
531 instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
532
533 instSkolTyCoVarX :: (Unique -> Name -> Kind -> TyCoVar)
534 -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
535 instSkolTyCoVarX mk_tcv subst tycovar
536 = do { uniq <- newUnique -- using a new unique is critical. See
537 -- Note [Skolems in zonkSyntaxExpr] in TcHsSyn
538 ; let new_tcv = mk_tcv uniq old_name kind
539 subst1 | isTyVar new_tcv
540 = extendTvSubstWithClone subst tycovar new_tcv
541 | otherwise
542 = extendCvSubstWithClone subst tycovar new_tcv
543 ; return (subst1, new_tcv) }
544 where
545 old_name = tyVarName tycovar
546 kind = substTyUnchecked subst (tyVarKind tycovar)
547
548 newFskTyVar :: TcType -> TcM TcTyVar
549 newFskTyVar fam_ty
550 = do { uniq <- newUnique
551 ; let name = mkSysTvName uniq (fsLit "fsk")
552 ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
553 {-
554 Note [Kind substitution when instantiating]
555 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
556 When we instantiate a bunch of kind and type variables, first we
557 expect them to be topologically sorted.
558 Then we have to instantiate the kind variables, build a substitution
559 from old variables to the new variables, then instantiate the type
560 variables substituting the original kind.
561
562 Exemple: If we want to instantiate
563 [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
564 we want
565 [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
566 instead of the buggous
567 [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
568
569
570 ************************************************************************
571 * *
572 MetaTvs (meta type variables; mutable)
573 * *
574 ************************************************************************
575 -}
576
577 mkMetaTyVarName :: Unique -> FastString -> Name
578 -- Makes a /System/ Name, which is eagerly eliminated by
579 -- the unifier; see TcUnify.nicer_to_update_tv1, and
580 -- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
581 mkMetaTyVarName uniq str = mkSysTvName uniq str
582
583 newSigTyVar :: Name -> Kind -> TcM TcTyVar
584 newSigTyVar name kind
585 = do { details <- newMetaDetails SigTv
586 ; return (mkTcTyVar name kind details) }
587
588 newFmvTyVar :: TcType -> TcM TcTyVar
589 -- Very like newMetaTyVar, except sets mtv_tclvl to one less
590 -- so that the fmv is untouchable.
591 newFmvTyVar fam_ty
592 = do { uniq <- newUnique
593 ; ref <- newMutVar Flexi
594 ; cur_lvl <- getTcLevel
595 ; let details = MetaTv { mtv_info = FlatMetaTv
596 , mtv_ref = ref
597 , mtv_tclvl = fmvTcLevel cur_lvl }
598 name = mkMetaTyVarName uniq (fsLit "s")
599 ; return (mkTcTyVar name (typeKind fam_ty) details) }
600
601 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
602 newMetaDetails info
603 = do { ref <- newMutVar Flexi
604 ; tclvl <- getTcLevel
605 ; return (MetaTv { mtv_info = info
606 , mtv_ref = ref
607 , mtv_tclvl = tclvl }) }
608
609 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
610 cloneMetaTyVar tv
611 = ASSERT( isTcTyVar tv )
612 do { uniq <- newUnique
613 ; ref <- newMutVar Flexi
614 ; let name' = setNameUnique (tyVarName tv) uniq
615 details' = case tcTyVarDetails tv of
616 details@(MetaTv {}) -> details { mtv_ref = ref }
617 _ -> pprPanic "cloneMetaTyVar" (ppr tv)
618 ; return (mkTcTyVar name' (tyVarKind tv) details') }
619
620 -- Works for both type and kind variables
621 readMetaTyVar :: TyVar -> TcM MetaDetails
622 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
623 readMutVar (metaTvRef tyvar)
624
625 isFilledMetaTyVar :: TyVar -> TcM Bool
626 -- True of a filled-in (Indirect) meta type variable
627 isFilledMetaTyVar tv
628 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
629 = do { details <- readMutVar ref
630 ; return (isIndirect details) }
631 | otherwise = return False
632
633 isUnfilledMetaTyVar :: TyVar -> TcM Bool
634 -- True of a un-filled-in (Flexi) meta type variable
635 isUnfilledMetaTyVar tv
636 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
637 = do { details <- readMutVar ref
638 ; return (isFlexi details) }
639 | otherwise = return False
640
641 --------------------
642 -- Works with both type and kind variables
643 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
644 -- Write into a currently-empty MetaTyVar
645
646 writeMetaTyVar tyvar ty
647 | not debugIsOn
648 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
649
650 -- Everything from here on only happens if DEBUG is on
651 | not (isTcTyVar tyvar)
652 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
653 return ()
654
655 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
656 = writeMetaTyVarRef tyvar ref ty
657
658 | otherwise
659 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
660 return ()
661
662 --------------------
663 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
664 -- Here the tyvar is for error checking only;
665 -- the ref cell must be for the same tyvar
666 writeMetaTyVarRef tyvar ref ty
667 | not debugIsOn
668 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
669 <+> text ":=" <+> ppr ty)
670 ; writeTcRef ref (Indirect ty) }
671
672 -- Everything from here on only happens if DEBUG is on
673 | otherwise
674 = do { meta_details <- readMutVar ref;
675 -- Zonk kinds to allow the error check to work
676 ; zonked_tv_kind <- zonkTcType tv_kind
677 ; zonked_ty_kind <- zonkTcType ty_kind
678
679 -- Check for double updates
680 ; ASSERT2( isFlexi meta_details,
681 hang (text "Double update of meta tyvar")
682 2 (ppr tyvar $$ ppr meta_details) )
683
684 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
685 ; writeMutVar ref (Indirect ty)
686 ; when ( not (isPredTy tv_kind)
687 -- Don't check kinds for updates to coercion variables
688 && not (zonked_ty_kind `tcEqKind` zonked_tv_kind))
689 $ WARN( True, hang (text "Ill-kinded update to meta tyvar")
690 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
691 <+> text ":="
692 <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) ) )
693 (return ()) }
694 where
695 tv_kind = tyVarKind tyvar
696 ty_kind = typeKind ty
697
698 {-
699 % Generating fresh variables for pattern match check
700 -}
701
702 -- UNINSTANTIATED VERSION OF tcInstSkolTyCoVars
703 genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar]
704 -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
705 -- Precondition: tyvars should be scoping-ordered
706 -- see Note [Kind substitution when instantiating]
707 -- Get the location from the monad; this is a complete freshening operation
708 genInstSkolTyVarsX loc subst tvs = instSkolTyCoVarsX (mkTcSkolTyVar loc False) subst tvs
709
710 {-
711 ************************************************************************
712 * *
713 MetaTvs: TauTvs
714 * *
715 ************************************************************************
716
717 Note [Never need to instantiate coercion variables]
718 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
719 With coercion variables sloshing around in types, it might seem that we
720 sometimes need to instantiate coercion variables. This would be problematic,
721 because coercion variables inhabit unboxed equality (~#), and the constraint
722 solver thinks in terms only of boxed equality (~). The solution is that
723 we never need to instantiate coercion variables in the first place.
724
725 The tyvars that we need to instantiate come from the types of functions,
726 data constructors, and patterns. These will never be quantified over
727 coercion variables, except for the special case of the promoted Eq#. But,
728 that can't ever appear in user code, so we're safe!
729 -}
730
731 newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
732 -- Make a new meta tyvar out of thin air
733 newAnonMetaTyVar meta_info kind
734 = do { uniq <- newUnique
735 ; let name = mkMetaTyVarName uniq s
736 s = case meta_info of
737 TauTv -> fsLit "t"
738 FlatMetaTv -> fsLit "fmv"
739 SigTv -> fsLit "a"
740 ; details <- newMetaDetails meta_info
741 ; return (mkTcTyVar name kind details) }
742
743 newFlexiTyVar :: Kind -> TcM TcTyVar
744 newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
745
746 newFlexiTyVarTy :: Kind -> TcM TcType
747 newFlexiTyVarTy kind = do
748 tc_tyvar <- newFlexiTyVar kind
749 return (mkTyVarTy tc_tyvar)
750
751 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
752 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
753
754 -- | Create a tyvar that can be a lifted or unlifted type.
755 newOpenFlexiTyVarTy :: TcM TcType
756 newOpenFlexiTyVarTy
757 = do { rr <- newFlexiTyVarTy runtimeRepTy
758 ; newFlexiTyVarTy (tYPE rr) }
759
760 newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
761 newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
762
763 newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
764 -- Instantiate with META type variables
765 -- Note that this works for a sequence of kind, type, and coercion variables
766 -- variables. Eg [ (k:*), (a:k->k) ]
767 -- Gives [ (k7:*), (a8:k7->k7) ]
768 newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
769 -- emptyTCvSubst has an empty in-scope set, but that's fine here
770 -- Since the tyvars are freshly made, they cannot possibly be
771 -- captured by any existing for-alls.
772
773 newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
774 -- Make a new unification variable tyvar whose Name and Kind come from
775 -- an existing TyVar. We substitute kind variables in the kind.
776 newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
777
778 newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
779 -- Just like newMetaTyVarX, but make a SigTv
780 newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar
781
782 new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
783 new_meta_tv_x info subst tyvar
784 = do { uniq <- newUnique
785 ; details <- newMetaDetails info
786 ; let name = mkSystemName uniq (getOccName tyvar)
787 -- See Note [Name of an instantiated type variable]
788 kind = substTyUnchecked subst (tyVarKind tyvar)
789 new_tv = mkTcTyVar name kind details
790 subst1 = extendTvSubstWithClone subst tyvar new_tv
791 ; return (subst1, new_tv) }
792
793 {- Note [Name of an instantiated type variable]
794 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
795 At the moment we give a unification variable a System Name, which
796 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
797
798 ************************************************************************
799 * *
800 Quantification
801 * *
802 ************************************************************************
803
804 Note [quantifyTyVars]
805 ~~~~~~~~~~~~~~~~~~~~~
806 quantifyTyVars is given the free vars of a type that we
807 are about to wrap in a forall.
808
809 It takes these free type/kind variables (partitioned into dependent and
810 non-dependent variables) and
811 1. Zonks them and remove globals and covars
812 2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
813 3. Calls zonkQuantifiedTyVar on each
814
815 Step (2) is often unimportant, because the kind variable is often
816 also free in the type. Eg
817 Typeable k (a::k)
818 has free vars {k,a}. But the type (see Trac #7916)
819 (f::k->*) (a::k)
820 has free vars {f,a}, but we must add 'k' as well! Hence step (3).
821
822 This function bothers to distinguish between dependent and non-dependent
823 variables only to keep correct defaulting behavior with -XNoPolyKinds.
824 With -XPolyKinds, it treats both classes of variables identically.
825
826 Note that this function can accept covars, but will never return them.
827 This is because we never want to infer a quantified covar!
828 -}
829
830 quantifyTyVars :: TcTyCoVarSet -- global tvs
831 -> Pair TcTyCoVarSet -- dependent tvs We only distinguish
832 -- nondependent tvs between these for
833 -- -XNoPolyKinds
834 -> TcM [TcTyVar]
835 -- See Note [quantifyTyVars]
836 -- Can be given a mixture of TcTyVars and TyVars, in the case of
837 -- associated type declarations. Also accepts covars, but *never* returns any.
838
839 quantifyTyVars gbl_tvs (Pair dep_tkvs nondep_tkvs)
840 = do { dep_tkvs <- zonkTyCoVarsAndFV dep_tkvs
841 ; nondep_tkvs <- (`minusVarSet` dep_tkvs) <$>
842 zonkTyCoVarsAndFV nondep_tkvs
843 ; gbl_tvs <- zonkTyCoVarsAndFV gbl_tvs
844
845 ; let all_cvs = filterVarSet isCoVar $
846 dep_tkvs `unionVarSet` nondep_tkvs `minusVarSet` gbl_tvs
847 dep_kvs = varSetElemsWellScoped $
848 dep_tkvs `minusVarSet` gbl_tvs
849 `minusVarSet` (closeOverKinds all_cvs)
850 -- remove any tvs that a covar depends on
851
852 nondep_tvs = varSetElemsWellScoped $
853 nondep_tkvs `minusVarSet` gbl_tvs
854 -- no worry about dependent cvs here, as these vars
855 -- are non-dependent
856
857 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
858
859 -- In the non-PolyKinds case, default the kind variables
860 -- to *, and zonk the tyvars as usual. Notice that this
861 -- may make quantifyTyVars return a shorter list
862 -- than it was passed, but that's ok
863 ; poly_kinds <- xoptM LangExt.PolyKinds
864 ; dep_vars2 <- if poly_kinds
865 then return dep_kvs
866 else do { let (meta_kvs, skolem_kvs) = partition is_meta dep_kvs
867 is_meta kv = isTcTyVar kv && isMetaTyVar kv
868
869 ; mapM_ defaultKindVar meta_kvs
870 ; return skolem_kvs } -- should be empty
871
872 ; let quant_vars = dep_vars2 ++ nondep_tvs
873
874 ; traceTc "quantifyTyVars"
875 (vcat [ text "globals:" <+> ppr gbl_tvs
876 , text "nondep:" <+> ppr nondep_tvs
877 , text "dep:" <+> ppr dep_kvs
878 , text "dep2:" <+> ppr dep_vars2
879 , text "quant_vars:" <+> ppr quant_vars ])
880
881 ; mapMaybeM zonk_quant quant_vars }
882 -- Because of the order, any kind variables
883 -- mentioned in the kinds of the type variables refer to
884 -- the now-quantified versions
885 where
886 zonk_quant tkv
887 | isTcTyVar tkv = zonkQuantifiedTyVar tkv
888 | otherwise = return $ Just tkv
889 -- For associated types, we have the class variables
890 -- in scope, and they are TyVars not TcTyVars
891
892 zonkQuantifiedTyVar :: TcTyVar -> TcM (Maybe TcTyVar)
893 -- The quantified type variables often include meta type variables
894 -- we want to freeze them into ordinary type variables, and
895 -- default their kind (e.g. from TYPE v to TYPE Lifted)
896 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
897 -- bound occurrences of the original type variable will get zonked to
898 -- the immutable version.
899 --
900 -- We leave skolem TyVars alone; they are immutable.
901 --
902 -- This function is called on both kind and type variables,
903 -- but kind variables *only* if PolyKinds is on.
904 --
905 -- This returns a tyvar if it should be quantified over; otherwise,
906 -- it returns Nothing. Nothing is
907 -- returned only if zonkQuantifiedTyVar is passed a RuntimeRep meta-tyvar,
908 -- in order to default to PtrRepLifted.
909 zonkQuantifiedTyVar tv = left_only `liftM` zonkQuantifiedTyVarOrType tv
910 where left_only :: Either a b -> Maybe a
911 left_only (Left x) = Just x
912 left_only (Right _) = Nothing
913
914 -- | Like zonkQuantifiedTyVar, but if zonking reveals that the tyvar
915 -- should become a type (when defaulting a RuntimeRep var to PtrRepLifted), it
916 -- returns the type instead.
917 zonkQuantifiedTyVarOrType :: TcTyVar -> TcM (Either TcTyVar TcType)
918 zonkQuantifiedTyVarOrType tv
919 = case tcTyVarDetails tv of
920 SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
921 ; return $ Left $ setTyVarKind tv kind }
922 -- It might be a skolem type variable,
923 -- for example from a user type signature
924
925 MetaTv { mtv_ref = ref } ->
926 do when debugIsOn $ do
927 -- [Sept 04] Check for non-empty.
928 -- See note [Silly Type Synonym]
929 cts <- readMutVar ref
930 case cts of
931 Flexi -> return ()
932 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
933 return ()
934 if isRuntimeRepVar tv
935 then do { writeMetaTyVar tv ptrRepLiftedTy
936 ; return (Right ptrRepLiftedTy) }
937 else Left `liftM` skolemiseUnboundMetaTyVar tv vanillaSkolemTv
938 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
939
940 -- | Take an (unconstrained) meta tyvar and default it. Works only on
941 -- vars of type RuntimeRep and of type *. For other kinds, it issues
942 -- an error. See Note [Defaulting with -XNoPolyKinds]
943 defaultKindVar :: TcTyVar -> TcM Kind
944 defaultKindVar kv
945 | ASSERT( isMetaTyVar kv )
946 isRuntimeRepVar kv
947 = writeMetaTyVar kv ptrRepLiftedTy >> return ptrRepLiftedTy
948 | isStarKind (tyVarKind kv)
949 = writeMetaTyVar kv liftedTypeKind >> return liftedTypeKind
950 | otherwise
951 = do { addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
952 , text "of kind:" <+> ppr (tyVarKind kv')
953 , text "Perhaps enable PolyKinds or add a kind signature" ])
954 ; return (mkTyVarTy kv) }
955 where
956 (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
957
958 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
959 -- We have a Meta tyvar with a ref-cell inside it
960 -- Skolemise it, so that
961 -- we are totally out of Meta-tyvar-land
962 -- We create a skolem TyVar, not a regular TyVar
963 -- See Note [Zonking to Skolem]
964 skolemiseUnboundMetaTyVar tv details
965 = ASSERT2( isMetaTyVar tv, ppr tv )
966 do { span <- getSrcSpanM -- Get the location from "here"
967 -- ie where we are generalising
968 ; kind <- zonkTcType (tyVarKind tv)
969 ; let uniq = getUnique tv
970 -- NB: Use same Unique as original tyvar. This is
971 -- important for TcHsType.splitTelescopeTvs to work properly
972
973 tv_name = getOccName tv
974 final_name = mkInternalName uniq tv_name span
975 final_tv = mkTcTyVar final_name kind details
976
977 ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
978 ; writeMetaTyVar tv (mkTyVarTy final_tv)
979 ; return final_tv }
980
981 {-
982 Note [Defaulting with -XNoPolyKinds]
983 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
984 Consider
985
986 data Compose f g a = Mk (f (g a))
987
988 We infer
989
990 Compose :: forall k1 k2. (k2 -> *) -> (k1 -> k2) -> k1 -> *
991 Mk :: forall k1 k2 (f :: k2 -> *) (g :: k1 -> k2) (a :: k1).
992 f (g a) -> Compose k1 k2 f g a
993
994 Now, in another module, we have -XNoPolyKinds -XDataKinds in effect.
995 What does 'Mk mean? Pre GHC-8.0 with -XNoPolyKinds,
996 we just defaulted all kind variables to *. But that's no good here,
997 because the kind variables in 'Mk aren't of kind *, so defaulting to *
998 is ill-kinded.
999
1000 After some debate on #11334, we decided to issue an error in this case.
1001 The code is in defaultKindVar.
1002
1003 Note [What is a meta variable?]
1004 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1005 A "meta type-variable", also know as a "unification variable" is a placeholder
1006 introduced by the typechecker for an as-yet-unknown monotype.
1007
1008 For example, when we see a call `reverse (f xs)`, we know that we calling
1009 reverse :: forall a. [a] -> [a]
1010 So we know that the argument `f xs` must be a "list of something". But what is
1011 the "something"? We don't know until we explore the `f xs` a bit more. So we set
1012 out what we do know at the call of `reverse` by instantiate its type with a fresh
1013 meta tyvar, `alpha` say. So now the type of the argument `f xs`, and of the
1014 result, is `[alpha]`. The unification variable `alpha` stands for the
1015 as-yet-unknown type of the elements of the list.
1016
1017 As type inference progresses we may learn more about `alpha`. For example, suppose
1018 `f` has the type
1019 f :: forall b. b -> [Maybe b]
1020 Then we instantiate `f`'s type with another fresh unification variable, say
1021 `beta`; and equate `f`'s result type with reverse's argument type, thus
1022 `[alpha] ~ [Maybe beta]`.
1023
1024 Now we can solve this equality to learn that `alpha ~ Maybe beta`, so we've
1025 refined our knowledge about `alpha`. And so on.
1026
1027 If you found this Note useful, you may also want to have a look at
1028 Section 5 of "Practical type inference for higher rank types" (Peyton Jones,
1029 Vytiniotis, Weirich and Shields. J. Functional Programming. 2011).
1030
1031 Note [What is zonking?]
1032 ~~~~~~~~~~~~~~~~~~~~~~~
1033 GHC relies heavily on mutability in the typechecker for efficient operation.
1034 For this reason, throughout much of the type checking process meta type
1035 variables (the MetaTv constructor of TcTyVarDetails) are represented by mutable
1036 variables (known as TcRefs).
1037
1038 Zonking is the process of ripping out these mutable variables and replacing them
1039 with a real TcType. This involves traversing the entire type expression, but the
1040 interesting part of replacing the mutable variables occurs in zonkTyVarOcc.
1041
1042 There are two ways to zonk a Type:
1043
1044 * zonkTcTypeToType, which is intended to be used at the end of type-checking
1045 for the final zonk. It has to deal with unfilled metavars, either by filling
1046 it with a value like Any or failing (determined by the UnboundTyVarZonker
1047 used).
1048
1049 * zonkTcType, which will happily ignore unfilled metavars. This is the
1050 appropriate function to use while in the middle of type-checking.
1051
1052 Note [Zonking to Skolem]
1053 ~~~~~~~~~~~~~~~~~~~~~~~~
1054 We used to zonk quantified type variables to regular TyVars. However, this
1055 leads to problems. Consider this program from the regression test suite:
1056
1057 eval :: Int -> String -> String -> String
1058 eval 0 root actual = evalRHS 0 root actual
1059
1060 evalRHS :: Int -> a
1061 evalRHS 0 root actual = eval 0 root actual
1062
1063 It leads to the deferral of an equality (wrapped in an implication constraint)
1064
1065 forall a. () => ((String -> String -> String) ~ a)
1066
1067 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
1068 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
1069 This has the *side effect* of also zonking the `a' in the deferred equality
1070 (which at this point is being handed around wrapped in an implication
1071 constraint).
1072
1073 Finally, the equality (with the zonked `a') will be handed back to the
1074 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
1075 If we zonk `a' with a regular type variable, we will have this regular type
1076 variable now floating around in the simplifier, which in many places assumes to
1077 only see proper TcTyVars.
1078
1079 We can avoid this problem by zonking with a skolem. The skolem is rigid
1080 (which we require for a quantified variable), but is still a TcTyVar that the
1081 simplifier knows how to deal with.
1082
1083 Note [Silly Type Synonyms]
1084 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1085 Consider this:
1086 type C u a = u -- Note 'a' unused
1087
1088 foo :: (forall a. C u a -> C u a) -> u
1089 foo x = ...
1090
1091 bar :: Num u => u
1092 bar = foo (\t -> t + t)
1093
1094 * From the (\t -> t+t) we get type {Num d} => d -> d
1095 where d is fresh.
1096
1097 * Now unify with type of foo's arg, and we get:
1098 {Num (C d a)} => C d a -> C d a
1099 where a is fresh.
1100
1101 * Now abstract over the 'a', but float out the Num (C d a) constraint
1102 because it does not 'really' mention a. (see exactTyVarsOfType)
1103 The arg to foo becomes
1104 \/\a -> \t -> t+t
1105
1106 * So we get a dict binding for Num (C d a), which is zonked to give
1107 a = ()
1108 [Note Sept 04: now that we are zonking quantified type variables
1109 on construction, the 'a' will be frozen as a regular tyvar on
1110 quantification, so the floated dict will still have type (C d a).
1111 Which renders this whole note moot; happily!]
1112
1113 * Then the \/\a abstraction has a zonked 'a' in it.
1114
1115 All very silly. I think its harmless to ignore the problem. We'll end up with
1116 a \/\a in the final result but all the occurrences of a will be zonked to ()
1117
1118 ************************************************************************
1119 * *
1120 Zonking types
1121 * *
1122 ************************************************************************
1123
1124 -}
1125
1126 -- | @tcGetGlobalTyCoVars@ returns a fully-zonked set of *scoped* tyvars free in
1127 -- the environment. To improve subsequent calls to the same function it writes
1128 -- the zonked set back into the environment. Note that this returns all
1129 -- variables free in anything (term-level or type-level) in scope. We thus
1130 -- don't have to worry about clashes with things that are not in scope, because
1131 -- if they are reachable, then they'll be returned here.
1132 tcGetGlobalTyCoVars :: TcM TcTyVarSet
1133 tcGetGlobalTyCoVars
1134 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
1135 ; gbl_tvs <- readMutVar gtv_var
1136 ; gbl_tvs' <- zonkTyCoVarsAndFV gbl_tvs
1137 ; writeMutVar gtv_var gbl_tvs'
1138 ; return gbl_tvs' }
1139
1140 zonkTcTypeAndFV :: TcType -> TcM TyCoVarSet
1141 -- Zonk a type and take its free variables
1142 -- With kind polymorphism it can be essential to zonk *first*
1143 -- so that we find the right set of free variables. Eg
1144 -- forall k1. forall (a:k2). a
1145 -- where k2:=k1 is in the substitution. We don't want
1146 -- k2 to look free in this type!
1147 -- NB: This might be called from within the knot, so don't use
1148 -- smart constructors. See Note [Zonking within the knot] in TcHsType
1149 zonkTcTypeAndFV ty
1150 = tyCoVarsOfType <$> mapType (zonkTcTypeMapper { tcm_smart = False }) () ty
1151
1152 zonkTyCoVar :: TyCoVar -> TcM TcType
1153 -- Works on TyVars and TcTyVars
1154 zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
1155 | isTyVar tv = mkTyVarTy <$> zonkTyCoVarKind tv
1156 | otherwise = ASSERT2( isCoVar tv, ppr tv )
1157 mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
1158 -- Hackily, when typechecking type and class decls
1159 -- we have TyVars in scopeadded (only) in
1160 -- TcHsType.tcTyClTyVars, but it seems
1161 -- painful to make them into TcTyVars there
1162
1163 zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
1164 zonkTyCoVarsAndFV tycovars = tyCoVarsOfTypes <$> mapM zonkTyCoVar (varSetElems tycovars)
1165
1166 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
1167 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
1168
1169 ----------------- Types
1170 zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
1171 zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
1172 ; return (setTyVarKind tv kind') }
1173
1174 zonkTcTypes :: [TcType] -> TcM [TcType]
1175 zonkTcTypes tys = mapM zonkTcType tys
1176
1177 {-
1178 ************************************************************************
1179 * *
1180 Zonking constraints
1181 * *
1182 ************************************************************************
1183 -}
1184
1185 zonkImplication :: Implication -> TcM Implication
1186 zonkImplication implic@(Implic { ic_skols = skols
1187 , ic_given = given
1188 , ic_wanted = wanted
1189 , ic_info = info })
1190 = do { skols' <- mapM zonkTcTyCoVarBndr skols -- Need to zonk their kinds!
1191 -- as Trac #7230 showed
1192 ; given' <- mapM zonkEvVar given
1193 ; info' <- zonkSkolemInfo info
1194 ; wanted' <- zonkWCRec wanted
1195 ; return (implic { ic_skols = skols'
1196 , ic_given = given'
1197 , ic_wanted = wanted'
1198 , ic_info = info' }) }
1199
1200 zonkEvVar :: EvVar -> TcM EvVar
1201 zonkEvVar var = do { ty' <- zonkTcType (varType var)
1202 ; return (setVarType var ty') }
1203
1204
1205 zonkWC :: WantedConstraints -> TcM WantedConstraints
1206 zonkWC wc = zonkWCRec wc
1207
1208 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
1209 zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
1210 = do { simple' <- zonkSimples simple
1211 ; implic' <- mapBagM zonkImplication implic
1212 ; insol' <- zonkSimples insol
1213 ; return (WC { wc_simple = simple', wc_impl = implic', wc_insol = insol' }) }
1214
1215 zonkSimples :: Cts -> TcM Cts
1216 zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
1217 ; traceTc "zonkSimples done:" (ppr cts')
1218 ; return cts' }
1219
1220 zonkCt' :: Ct -> TcM Ct
1221 zonkCt' ct = zonkCt ct
1222
1223 zonkCt :: Ct -> TcM Ct
1224 zonkCt ct@(CHoleCan { cc_ev = ev })
1225 = do { ev' <- zonkCtEvidence ev
1226 ; return $ ct { cc_ev = ev' } }
1227 zonkCt ct
1228 = do { fl' <- zonkCtEvidence (cc_ev ct)
1229 ; return (mkNonCanonical fl') }
1230
1231 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
1232 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
1233 = do { pred' <- zonkTcType pred
1234 ; return (ctev { ctev_pred = pred'}) }
1235 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest })
1236 = do { pred' <- zonkTcType pred
1237 ; let dest' = case dest of
1238 EvVarDest ev -> EvVarDest $ setVarType ev pred'
1239 -- necessary in simplifyInfer
1240 HoleDest h -> HoleDest h
1241 ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
1242 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
1243 = do { pred' <- zonkTcType pred
1244 ; return (ctev { ctev_pred = pred' }) }
1245
1246 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
1247 zonkSkolemInfo (SigSkol cx ty) = do { ty <- readExpType ty
1248 ; ty' <- zonkTcType ty
1249 ; return (SigSkol cx (mkCheckExpType ty')) }
1250 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
1251 ; return (InferSkol ntys') }
1252 where
1253 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
1254 zonkSkolemInfo skol_info = return skol_info
1255
1256 {-
1257 %************************************************************************
1258 %* *
1259 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
1260 * *
1261 * For internal use only! *
1262 * *
1263 ************************************************************************
1264
1265 -}
1266
1267 -- zonkId is used *during* typechecking just to zonk the Id's type
1268 zonkId :: TcId -> TcM TcId
1269 zonkId id
1270 = do { ty' <- zonkTcType (idType id)
1271 ; return (Id.setIdType id ty') }
1272
1273 -- | A suitable TyCoMapper for zonking a type inside the knot, and
1274 -- before all metavars are filled in.
1275 zonkTcTypeMapper :: TyCoMapper () TcM
1276 zonkTcTypeMapper = TyCoMapper
1277 { tcm_smart = True
1278 , tcm_tyvar = const zonkTcTyVar
1279 , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
1280 , tcm_hole = hole
1281 , tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv }
1282 where
1283 hole :: () -> CoercionHole -> Role -> Type -> Type
1284 -> TcM Coercion
1285 hole _ h r t1 t2
1286 = do { contents <- unpackCoercionHole_maybe h
1287 ; case contents of
1288 Just co -> do { co <- zonkCo co
1289 ; checkCoercionHole co h r t1 t2 }
1290 Nothing -> do { t1 <- zonkTcType t1
1291 ; t2 <- zonkTcType t2
1292 ; return $ mkHoleCo h r t1 t2 } }
1293
1294
1295 -- For unbound, mutable tyvars, zonkType uses the function given to it
1296 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
1297 -- type variable and zonks the kind too
1298 zonkTcType :: TcType -> TcM TcType
1299 zonkTcType = mapType zonkTcTypeMapper ()
1300
1301 -- | "Zonk" a coercion -- really, just zonk any types in the coercion
1302 zonkCo :: Coercion -> TcM Coercion
1303 zonkCo = mapCoercion zonkTcTypeMapper ()
1304
1305 zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
1306 -- A tyvar binder is never a unification variable (MetaTv),
1307 -- rather it is always a skolems. BUT it may have a kind
1308 -- that has not yet been zonked, and may include kind
1309 -- unification variables.
1310 zonkTcTyCoVarBndr tyvar
1311 -- can't use isCoVar, because it looks at a TyCon. Argh.
1312 = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), ppr tyvar ) do
1313 updateTyVarKindM zonkTcType tyvar
1314
1315 -- | Zonk a TyBinder
1316 zonkTcTyBinder :: TcTyBinder -> TcM TcTyBinder
1317 zonkTcTyBinder (Anon ty) = Anon <$> zonkTcType ty
1318 zonkTcTyBinder (Named tv vis) = Named <$> zonkTcTyCoVarBndr tv <*> pure vis
1319
1320 zonkTcTyVar :: TcTyVar -> TcM TcType
1321 -- Simply look through all Flexis
1322 zonkTcTyVar tv
1323 | isTcTyVar tv
1324 = case tcTyVarDetails tv of
1325 SkolemTv {} -> zonk_kind_and_return
1326 RuntimeUnk {} -> zonk_kind_and_return
1327 FlatSkol ty -> zonkTcType ty
1328 MetaTv { mtv_ref = ref }
1329 -> do { cts <- readMutVar ref
1330 ; case cts of
1331 Flexi -> zonk_kind_and_return
1332 Indirect ty -> zonkTcType ty }
1333
1334 | otherwise -- coercion variable
1335 = zonk_kind_and_return
1336 where
1337 zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv
1338 ; return (mkTyVarTy z_tv) }
1339
1340 {-
1341 %************************************************************************
1342 %* *
1343 Tidying
1344 * *
1345 ************************************************************************
1346 -}
1347
1348 zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
1349 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
1350 ; return (tidyOpenType env ty') }
1351
1352 -- | Make an 'ErrorThing' storing a type.
1353 mkTypeErrorThing :: TcType -> ErrorThing
1354 mkTypeErrorThing ty = ErrorThing ty (Just $ length $ snd $ repSplitAppTys ty)
1355 zonkTidyTcType
1356 -- NB: Use *rep*splitAppTys, else we get #11313
1357
1358 -- | Make an 'ErrorThing' storing a type, with some extra args known about
1359 mkTypeErrorThingArgs :: TcType -> Int -> ErrorThing
1360 mkTypeErrorThingArgs ty num_args
1361 = ErrorThing ty (Just $ (length $ snd $ repSplitAppTys ty) + num_args)
1362 zonkTidyTcType
1363
1364 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
1365 zonkTidyOrigin env (GivenOrigin skol_info)
1366 = do { skol_info1 <- zonkSkolemInfo skol_info
1367 ; let skol_info2 = tidySkolemInfo env skol_info1
1368 ; return (env, GivenOrigin skol_info2) }
1369 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act
1370 , uo_expected = exp
1371 , uo_thing = m_thing })
1372 = do { (env1, act') <- zonkTidyTcType env act
1373 ; mb_exp <- readExpType_maybe exp -- it really should be filled in.
1374 -- unless we're debugging.
1375 ; (env2, exp') <- case mb_exp of
1376 Just ty -> second mkCheckExpType <$> zonkTidyTcType env1 ty
1377 Nothing -> return (env1, exp)
1378 ; (env3, m_thing') <- zonkTidyErrorThing env2 m_thing
1379 ; return ( env3, orig { uo_actual = act'
1380 , uo_expected = exp'
1381 , uo_thing = m_thing' }) }
1382 zonkTidyOrigin env (KindEqOrigin ty1 m_ty2 orig t_or_k)
1383 = do { (env1, ty1') <- zonkTidyTcType env ty1
1384 ; (env2, m_ty2') <- case m_ty2 of
1385 Just ty2 -> second Just <$> zonkTidyTcType env1 ty2
1386 Nothing -> return (env1, Nothing)
1387 ; (env3, orig') <- zonkTidyOrigin env2 orig
1388 ; return (env3, KindEqOrigin ty1' m_ty2' orig' t_or_k) }
1389 zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
1390 = do { (env1, p1') <- zonkTidyTcType env p1
1391 ; (env2, p2') <- zonkTidyTcType env1 p2
1392 ; return (env2, FunDepOrigin1 p1' l1 p2' l2) }
1393 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
1394 = do { (env1, p1') <- zonkTidyTcType env p1
1395 ; (env2, p2') <- zonkTidyTcType env1 p2
1396 ; (env3, o1') <- zonkTidyOrigin env2 o1
1397 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
1398 zonkTidyOrigin env orig = return (env, orig)
1399
1400 zonkTidyErrorThing :: TidyEnv -> Maybe ErrorThing
1401 -> TcM (TidyEnv, Maybe ErrorThing)
1402 zonkTidyErrorThing env (Just (ErrorThing thing n_args zonker))
1403 = do { (env', thing') <- zonker env thing
1404 ; return (env', Just $ ErrorThing thing' n_args zonker) }
1405 zonkTidyErrorThing env Nothing
1406 = return (env, Nothing)
1407
1408 ----------------
1409 tidyCt :: TidyEnv -> Ct -> Ct
1410 -- Used only in error reporting
1411 -- Also converts it to non-canonical
1412 tidyCt env ct
1413 = case ct of
1414 CHoleCan { cc_ev = ev }
1415 -> ct { cc_ev = tidy_ev env ev }
1416 _ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
1417 where
1418 tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
1419 -- NB: we do not tidy the ctev_evar field because we don't
1420 -- show it in error messages
1421 tidy_ev env ctev@(CtGiven { ctev_pred = pred })
1422 = ctev { ctev_pred = tidyType env pred }
1423 tidy_ev env ctev@(CtWanted { ctev_pred = pred })
1424 = ctev { ctev_pred = tidyType env pred }
1425 tidy_ev env ctev@(CtDerived { ctev_pred = pred })
1426 = ctev { ctev_pred = tidyType env pred }
1427
1428 ----------------
1429 tidyEvVar :: TidyEnv -> EvVar -> EvVar
1430 tidyEvVar env var = setVarType var (tidyType env (varType var))
1431
1432 ----------------
1433 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
1434 tidySkolemInfo env (DerivSkol ty) = DerivSkol (tidyType env ty)
1435 tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (mkCheckExpType $
1436 tidyType env $
1437 checkingExpType "tidySkolemInfo" ty)
1438 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
1439 tidySkolemInfo env (UnifyForAllSkol ty) = UnifyForAllSkol (tidyType env ty)
1440 tidySkolemInfo _ info = info