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