1-- (c) The University of Glasgow 2006 2 3{-# LANGUAGE CPP, DeriveDataTypeable #-} 4 5module TcEvidence ( 6 7 -- HsWrapper 8 HsWrapper(..), 9 (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, 10 mkWpLams, mkWpLet, mkWpCastN, mkWpCastR, collectHsWrapBinders, 11 mkWpFun, idHsWrapper, isIdHsWrapper, isErasableHsWrapper, 12 pprHsWrapper, 13 14 -- Evidence bindings 15 TcEvBinds(..), EvBindsVar(..), 16 EvBindMap(..), emptyEvBindMap, extendEvBinds, 17 lookupEvBind, evBindMapBinds, foldEvBindMap, filterEvBindMap, 18 isEmptyEvBindMap, 19 EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind, 20 evBindVar, isCoEvBindsVar, 21 22 -- EvTerm (already a CoreExpr) 23 EvTerm(..), EvExpr, 24 evId, evCoercion, evCast, evDFunApp, evDataConApp, evSelector, 25 mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, findNeededEvVars, 26 27 evTermCoercion, evTermCoercion_maybe, 28 EvCallStack(..), 29 EvTypeable(..), 30 31 -- TcCoercion 32 TcCoercion, TcCoercionR, TcCoercionN, TcCoercionP, CoercionHole, 33 TcMCoercion, 34 Role(..), LeftOrRight(..), pickLR, 35 mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo, 36 mkTcTyConAppCo, mkTcAppCo, mkTcFunCo, 37 mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos, 38 mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSubCo, 39 tcDowngradeRole, 40 mkTcAxiomRuleCo, mkTcGReflRightCo, mkTcGReflLeftCo, mkTcPhantomCo, 41 mkTcCoherenceLeftCo, 42 mkTcCoherenceRightCo, 43 mkTcKindCo, 44 tcCoercionKind, coVarsOfTcCo, 45 mkTcCoVarCo, 46 isTcReflCo, isTcReflexiveCo, isTcGReflMCo, tcCoToMCo, 47 tcCoercionRole, 48 unwrapIP, wrapIP 49 ) where 50#include "GhclibHsVersions.h" 51 52import GhcPrelude 53 54import Var 55import CoAxiom 56import Coercion 57import PprCore () -- Instance OutputableBndr TyVar 58import TcType 59import Type 60import TyCon 61import DataCon( DataCon, dataConWrapId ) 62import Class( Class ) 63import PrelNames 64import DynFlags ( gopt, GeneralFlag(Opt_PrintTypecheckerElaboration) ) 65import VarEnv 66import VarSet 67import Predicate 68import Name 69import Pair 70 71import CoreSyn 72import Class ( classSCSelId ) 73import CoreFVs ( exprSomeFreeVars ) 74 75import Util 76import Bag 77import qualified Data.Data as Data 78import Outputable 79import SrcLoc 80import Data.IORef( IORef ) 81import UniqSet 82 83{- 84Note [TcCoercions] 85~~~~~~~~~~~~~~~~~~ 86| TcCoercions are a hack used by the typechecker. Normally, 87Coercions have free variables of type (a ~# b): we call these 88CoVars. However, the type checker passes around equality evidence 89(boxed up) at type (a ~ b). 90 91An TcCoercion is simply a Coercion whose free variables have may be either 92boxed or unboxed. After we are done with typechecking the desugarer finds the 93boxed free variables, unboxes them, and creates a resulting real Coercion with 94kosher free variables. 95 96-} 97 98type TcCoercion = Coercion 99type TcCoercionN = CoercionN -- A Nominal coercion ~N 100type TcCoercionR = CoercionR -- A Representational coercion ~R 101type TcCoercionP = CoercionP -- a phantom coercion 102type TcMCoercion = MCoercion 103 104mkTcReflCo :: Role -> TcType -> TcCoercion 105mkTcSymCo :: TcCoercion -> TcCoercion 106mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion 107mkTcNomReflCo :: TcType -> TcCoercionN 108mkTcRepReflCo :: TcType -> TcCoercionR 109mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion 110mkTcAppCo :: TcCoercion -> TcCoercionN -> TcCoercion 111mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion 112mkTcAxInstCo :: Role -> CoAxiom br -> BranchIndex 113 -> [TcType] -> [TcCoercion] -> TcCoercion 114mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType] 115 -> [TcCoercion] -> TcCoercionR 116mkTcForAllCo :: TyVar -> TcCoercionN -> TcCoercion -> TcCoercion 117mkTcForAllCos :: [(TyVar, TcCoercionN)] -> TcCoercion -> TcCoercion 118mkTcNthCo :: Role -> Int -> TcCoercion -> TcCoercion 119mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion 120mkTcSubCo :: TcCoercionN -> TcCoercionR 121tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion 122mkTcAxiomRuleCo :: CoAxiomRule -> [TcCoercion] -> TcCoercionR 123mkTcGReflRightCo :: Role -> TcType -> TcCoercionN -> TcCoercion 124mkTcGReflLeftCo :: Role -> TcType -> TcCoercionN -> TcCoercion 125mkTcCoherenceLeftCo :: Role -> TcType -> TcCoercionN 126 -> TcCoercion -> TcCoercion 127mkTcCoherenceRightCo :: Role -> TcType -> TcCoercionN 128 -> TcCoercion -> TcCoercion 129mkTcPhantomCo :: TcCoercionN -> TcType -> TcType -> TcCoercionP 130mkTcKindCo :: TcCoercion -> TcCoercionN 131mkTcCoVarCo :: CoVar -> TcCoercion 132 133tcCoercionKind :: TcCoercion -> Pair TcType 134tcCoercionRole :: TcCoercion -> Role 135coVarsOfTcCo :: TcCoercion -> TcTyCoVarSet 136isTcReflCo :: TcCoercion -> Bool 137isTcGReflMCo :: TcMCoercion -> Bool 138 139-- | This version does a slow check, calculating the related types and seeing 140-- if they are equal. 141isTcReflexiveCo :: TcCoercion -> Bool 142 143mkTcReflCo = mkReflCo 144mkTcSymCo = mkSymCo 145mkTcTransCo = mkTransCo 146mkTcNomReflCo = mkNomReflCo 147mkTcRepReflCo = mkRepReflCo 148mkTcTyConAppCo = mkTyConAppCo 149mkTcAppCo = mkAppCo 150mkTcFunCo = mkFunCo 151mkTcAxInstCo = mkAxInstCo 152mkTcUnbranchedAxInstCo = mkUnbranchedAxInstCo Representational 153mkTcForAllCo = mkForAllCo 154mkTcForAllCos = mkForAllCos 155mkTcNthCo = mkNthCo 156mkTcLRCo = mkLRCo 157mkTcSubCo = mkSubCo 158tcDowngradeRole = downgradeRole 159mkTcAxiomRuleCo = mkAxiomRuleCo 160mkTcGReflRightCo = mkGReflRightCo 161mkTcGReflLeftCo = mkGReflLeftCo 162mkTcCoherenceLeftCo = mkCoherenceLeftCo 163mkTcCoherenceRightCo = mkCoherenceRightCo 164mkTcPhantomCo = mkPhantomCo 165mkTcKindCo = mkKindCo 166mkTcCoVarCo = mkCoVarCo 167 168tcCoercionKind = coercionKind 169tcCoercionRole = coercionRole 170coVarsOfTcCo = coVarsOfCo 171isTcReflCo = isReflCo 172isTcGReflMCo = isGReflMCo 173isTcReflexiveCo = isReflexiveCo 174 175tcCoToMCo :: TcCoercion -> TcMCoercion 176tcCoToMCo = coToMCo 177 178-- | If the EqRel is ReprEq, makes a SubCo; otherwise, does nothing. 179-- Note that the input coercion should always be nominal. 180maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion 181maybeTcSubCo NomEq = id 182maybeTcSubCo ReprEq = mkTcSubCo 183 184 185{- 186%************************************************************************ 187%* * 188 HsWrapper 189* * 190************************************************************************ 191-} 192 193data HsWrapper 194 = WpHole -- The identity coercion 195 196 | WpCompose HsWrapper HsWrapper 197 -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]] 198 -- 199 -- Hence (\a. []) `WpCompose` (\b. []) = (\a b. []) 200 -- But ([] a) `WpCompose` ([] b) = ([] b a) 201 202 | WpFun HsWrapper HsWrapper TcType SDoc 203 -- (WpFun wrap1 wrap2 t1)[e] = \(x:t1). wrap2[ e wrap1[x] ] 204 -- So note that if wrap1 :: exp_arg <= act_arg 205 -- wrap2 :: act_res <= exp_res 206 -- then WpFun wrap1 wrap2 : (act_arg -> arg_res) <= (exp_arg -> exp_res) 207 -- This isn't the same as for mkFunCo, but it has to be this way 208 -- because we can't use 'sym' to flip around these HsWrappers 209 -- The TcType is the "from" type of the first wrapper 210 -- The SDoc explains the circumstances under which we have created this 211 -- WpFun, in case we run afoul of levity polymorphism restrictions in 212 -- the desugarer. See Note [Levity polymorphism checking] in DsMonad 213 214 | WpCast TcCoercionR -- A cast: [] `cast` co 215 -- Guaranteed not the identity coercion 216 -- At role Representational 217 218 -- Evidence abstraction and application 219 -- (both dictionaries and coercions) 220 | WpEvLam EvVar -- \d. [] the 'd' is an evidence variable 221 | WpEvApp EvTerm -- [] d the 'd' is evidence for a constraint 222 -- Kind and Type abstraction and application 223 | WpTyLam TyVar -- \a. [] the 'a' is a type/kind variable (not coercion var) 224 | WpTyApp KindOrType -- [] t the 't' is a type (not coercion) 225 226 227 | WpLet TcEvBinds -- Non-empty (or possibly non-empty) evidence bindings, 228 -- so that the identity coercion is always exactly WpHole 229 230-- Cannot derive Data instance because SDoc is not Data (it stores a function). 231-- So we do it manually: 232instance Data.Data HsWrapper where 233 gfoldl _ z WpHole = z WpHole 234 gfoldl k z (WpCompose a1 a2) = z WpCompose `k` a1 `k` a2 235 gfoldl k z (WpFun a1 a2 a3 _) = z wpFunEmpty `k` a1 `k` a2 `k` a3 236 gfoldl k z (WpCast a1) = z WpCast `k` a1 237 gfoldl k z (WpEvLam a1) = z WpEvLam `k` a1 238 gfoldl k z (WpEvApp a1) = z WpEvApp `k` a1 239 gfoldl k z (WpTyLam a1) = z WpTyLam `k` a1 240 gfoldl k z (WpTyApp a1) = z WpTyApp `k` a1 241 gfoldl k z (WpLet a1) = z WpLet `k` a1 242 243 gunfold k z c = case Data.constrIndex c of 244 1 -> z WpHole 245 2 -> k (k (z WpCompose)) 246 3 -> k (k (k (z wpFunEmpty))) 247 4 -> k (z WpCast) 248 5 -> k (z WpEvLam) 249 6 -> k (z WpEvApp) 250 7 -> k (z WpTyLam) 251 8 -> k (z WpTyApp) 252 _ -> k (z WpLet) 253 254 toConstr WpHole = wpHole_constr 255 toConstr (WpCompose _ _) = wpCompose_constr 256 toConstr (WpFun _ _ _ _) = wpFun_constr 257 toConstr (WpCast _) = wpCast_constr 258 toConstr (WpEvLam _) = wpEvLam_constr 259 toConstr (WpEvApp _) = wpEvApp_constr 260 toConstr (WpTyLam _) = wpTyLam_constr 261 toConstr (WpTyApp _) = wpTyApp_constr 262 toConstr (WpLet _) = wpLet_constr 263 264 dataTypeOf _ = hsWrapper_dataType 265 266hsWrapper_dataType :: Data.DataType 267hsWrapper_dataType 268 = Data.mkDataType "HsWrapper" 269 [ wpHole_constr, wpCompose_constr, wpFun_constr, wpCast_constr 270 , wpEvLam_constr, wpEvApp_constr, wpTyLam_constr, wpTyApp_constr 271 , wpLet_constr] 272 273wpHole_constr, wpCompose_constr, wpFun_constr, wpCast_constr, wpEvLam_constr, 274 wpEvApp_constr, wpTyLam_constr, wpTyApp_constr, wpLet_constr :: Data.Constr 275wpHole_constr = mkHsWrapperConstr "WpHole" 276wpCompose_constr = mkHsWrapperConstr "WpCompose" 277wpFun_constr = mkHsWrapperConstr "WpFun" 278wpCast_constr = mkHsWrapperConstr "WpCast" 279wpEvLam_constr = mkHsWrapperConstr "WpEvLam" 280wpEvApp_constr = mkHsWrapperConstr "WpEvApp" 281wpTyLam_constr = mkHsWrapperConstr "WpTyLam" 282wpTyApp_constr = mkHsWrapperConstr "WpTyApp" 283wpLet_constr = mkHsWrapperConstr "WpLet" 284 285mkHsWrapperConstr :: String -> Data.Constr 286mkHsWrapperConstr name = Data.mkConstr hsWrapper_dataType name [] Data.Prefix 287 288wpFunEmpty :: HsWrapper -> HsWrapper -> TcType -> HsWrapper 289wpFunEmpty c1 c2 t1 = WpFun c1 c2 t1 empty 290 291(<.>) :: HsWrapper -> HsWrapper -> HsWrapper 292WpHole <.> c = c 293c <.> WpHole = c 294c1 <.> c2 = c1 `WpCompose` c2 295 296mkWpFun :: HsWrapper -> HsWrapper 297 -> TcType -- the "from" type of the first wrapper 298 -> TcType -- either type of the second wrapper (used only when the 299 -- second wrapper is the identity) 300 -> SDoc -- what caused you to want a WpFun? Something like "When converting ..." 301 -> HsWrapper 302mkWpFun WpHole WpHole _ _ _ = WpHole 303mkWpFun WpHole (WpCast co2) t1 _ _ = WpCast (mkTcFunCo Representational (mkTcRepReflCo t1) co2) 304mkWpFun (WpCast co1) WpHole _ t2 _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) (mkTcRepReflCo t2)) 305mkWpFun (WpCast co1) (WpCast co2) _ _ _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) co2) 306mkWpFun co1 co2 t1 _ d = WpFun co1 co2 t1 d 307 308mkWpCastR :: TcCoercionR -> HsWrapper 309mkWpCastR co 310 | isTcReflCo co = WpHole 311 | otherwise = ASSERT2(tcCoercionRole co == Representational, ppr co) 312 WpCast co 313 314mkWpCastN :: TcCoercionN -> HsWrapper 315mkWpCastN co 316 | isTcReflCo co = WpHole 317 | otherwise = ASSERT2(tcCoercionRole co == Nominal, ppr co) 318 WpCast (mkTcSubCo co) 319 -- The mkTcSubCo converts Nominal to Representational 320 321mkWpTyApps :: [Type] -> HsWrapper 322mkWpTyApps tys = mk_co_app_fn WpTyApp tys 323 324mkWpEvApps :: [EvTerm] -> HsWrapper 325mkWpEvApps args = mk_co_app_fn WpEvApp args 326 327mkWpEvVarApps :: [EvVar] -> HsWrapper 328mkWpEvVarApps vs = mk_co_app_fn WpEvApp (map (EvExpr . evId) vs) 329 330mkWpTyLams :: [TyVar] -> HsWrapper 331mkWpTyLams ids = mk_co_lam_fn WpTyLam ids 332 333mkWpLams :: [Var] -> HsWrapper 334mkWpLams ids = mk_co_lam_fn WpEvLam ids 335 336mkWpLet :: TcEvBinds -> HsWrapper 337-- This no-op is a quite a common case 338mkWpLet (EvBinds b) | isEmptyBag b = WpHole 339mkWpLet ev_binds = WpLet ev_binds 340 341mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper 342mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as 343 344mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper 345-- For applications, the *first* argument must 346-- come *last* in the composition sequence 347mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as 348 349idHsWrapper :: HsWrapper 350idHsWrapper = WpHole 351 352isIdHsWrapper :: HsWrapper -> Bool 353isIdHsWrapper WpHole = True 354isIdHsWrapper _ = False 355 356-- | Is the wrapper erasable, i.e., will not affect runtime semantics? 357isErasableHsWrapper :: HsWrapper -> Bool 358isErasableHsWrapper = go 359 where 360 go WpHole = True 361 go (WpCompose wrap1 wrap2) = go wrap1 && go wrap2 362 -- not so sure about WpFun. But it eta-expands, so... 363 go WpFun{} = False 364 go WpCast{} = True 365 go WpEvLam{} = False -- case in point 366 go WpEvApp{} = False 367 go WpTyLam{} = True 368 go WpTyApp{} = True 369 go WpLet{} = False 370 371collectHsWrapBinders :: HsWrapper -> ([Var], HsWrapper) 372-- Collect the outer lambda binders of a HsWrapper, 373-- stopping as soon as you get to a non-lambda binder 374collectHsWrapBinders wrap = go wrap [] 375 where 376 -- go w ws = collectHsWrapBinders (w <.> w1 <.> ... <.> wn) 377 go :: HsWrapper -> [HsWrapper] -> ([Var], HsWrapper) 378 go (WpEvLam v) wraps = add_lam v (gos wraps) 379 go (WpTyLam v) wraps = add_lam v (gos wraps) 380 go (WpCompose w1 w2) wraps = go w1 (w2:wraps) 381 go wrap wraps = ([], foldl' (<.>) wrap wraps) 382 383 gos [] = ([], WpHole) 384 gos (w:ws) = go w ws 385 386 add_lam v (vs,w) = (v:vs, w) 387 388{- 389************************************************************************ 390* * 391 Evidence bindings 392* * 393************************************************************************ 394-} 395 396data TcEvBinds 397 = TcEvBinds -- Mutable evidence bindings 398 EvBindsVar -- Mutable because they are updated "later" 399 -- when an implication constraint is solved 400 401 | EvBinds -- Immutable after zonking 402 (Bag EvBind) 403 404data EvBindsVar 405 = EvBindsVar { 406 ebv_uniq :: Unique, 407 -- The Unique is for debug printing only 408 409 ebv_binds :: IORef EvBindMap, 410 -- The main payload: the value-level evidence bindings 411 -- (dictionaries etc) 412 -- Some Given, some Wanted 413 414 ebv_tcvs :: IORef CoVarSet 415 -- The free Given coercion vars needed by Wanted coercions that 416 -- are solved by filling in their HoleDest in-place. Since they 417 -- don't appear in ebv_binds, we keep track of their free 418 -- variables so that we can report unused given constraints 419 -- See Note [Tracking redundant constraints] in TcSimplify 420 } 421 422 | CoEvBindsVar { -- See Note [Coercion evidence only] 423 424 -- See above for comments on ebv_uniq, ebv_tcvs 425 ebv_uniq :: Unique, 426 ebv_tcvs :: IORef CoVarSet 427 } 428 429instance Data.Data TcEvBinds where 430 -- Placeholder; we can't travers into TcEvBinds 431 toConstr _ = abstractConstr "TcEvBinds" 432 gunfold _ _ = error "gunfold" 433 dataTypeOf _ = Data.mkNoRepType "TcEvBinds" 434 435{- Note [Coercion evidence only] 436~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 437Class constraints etc give rise to /term/ bindings for evidence, and 438we have nowhere to put term bindings in /types/. So in some places we 439use CoEvBindsVar (see newCoTcEvBinds) to signal that no term-level 440evidence bindings are allowed. Notebly (): 441 442 - Places in types where we are solving kind constraints (all of which 443 are equalities); see solveEqualities, solveLocalEqualities 444 445 - When unifying forall-types 446-} 447 448isCoEvBindsVar :: EvBindsVar -> Bool 449isCoEvBindsVar (CoEvBindsVar {}) = True 450isCoEvBindsVar (EvBindsVar {}) = False 451 452----------------- 453newtype EvBindMap 454 = EvBindMap { 455 ev_bind_varenv :: DVarEnv EvBind 456 } -- Map from evidence variables to evidence terms 457 -- We use @DVarEnv@ here to get deterministic ordering when we 458 -- turn it into a Bag. 459 -- If we don't do that, when we generate let bindings for 460 -- dictionaries in dsTcEvBinds they will be generated in random 461 -- order. 462 -- 463 -- For example: 464 -- 465 -- let $dEq = GHC.Classes.$fEqInt in 466 -- let $$dNum = GHC.Num.$fNumInt in ... 467 -- 468 -- vs 469 -- 470 -- let $dNum = GHC.Num.$fNumInt in 471 -- let $dEq = GHC.Classes.$fEqInt in ... 472 -- 473 -- See Note [Deterministic UniqFM] in UniqDFM for explanation why 474 -- @UniqFM@ can lead to nondeterministic order. 475 476emptyEvBindMap :: EvBindMap 477emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyDVarEnv } 478 479extendEvBinds :: EvBindMap -> EvBind -> EvBindMap 480extendEvBinds bs ev_bind 481 = EvBindMap { ev_bind_varenv = extendDVarEnv (ev_bind_varenv bs) 482 (eb_lhs ev_bind) 483 ev_bind } 484 485isEmptyEvBindMap :: EvBindMap -> Bool 486isEmptyEvBindMap (EvBindMap m) = isEmptyDVarEnv m 487 488lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind 489lookupEvBind bs = lookupDVarEnv (ev_bind_varenv bs) 490 491evBindMapBinds :: EvBindMap -> Bag EvBind 492evBindMapBinds = foldEvBindMap consBag emptyBag 493 494foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a 495foldEvBindMap k z bs = foldDVarEnv k z (ev_bind_varenv bs) 496 497filterEvBindMap :: (EvBind -> Bool) -> EvBindMap -> EvBindMap 498filterEvBindMap k (EvBindMap { ev_bind_varenv = env }) 499 = EvBindMap { ev_bind_varenv = filterDVarEnv k env } 500 501instance Outputable EvBindMap where 502 ppr (EvBindMap m) = ppr m 503 504----------------- 505-- All evidence is bound by EvBinds; no side effects 506data EvBind 507 = EvBind { eb_lhs :: EvVar 508 , eb_rhs :: EvTerm 509 , eb_is_given :: Bool -- True <=> given 510 -- See Note [Tracking redundant constraints] in TcSimplify 511 } 512 513evBindVar :: EvBind -> EvVar 514evBindVar = eb_lhs 515 516mkWantedEvBind :: EvVar -> EvTerm -> EvBind 517mkWantedEvBind ev tm = EvBind { eb_is_given = False, eb_lhs = ev, eb_rhs = tm } 518 519-- EvTypeable are never given, so we can work with EvExpr here instead of EvTerm 520mkGivenEvBind :: EvVar -> EvTerm -> EvBind 521mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = tm } 522 523 524-- An EvTerm is, conceptually, a CoreExpr that implements the constraint. 525-- Unfortunately, we cannot just do 526-- type EvTerm = CoreExpr 527-- Because of staging problems issues around EvTypeable 528data EvTerm 529 = EvExpr EvExpr 530 531 | EvTypeable Type EvTypeable -- Dictionary for (Typeable ty) 532 533 | EvFun -- /\as \ds. let binds in v 534 { et_tvs :: [TyVar] 535 , et_given :: [EvVar] 536 , et_binds :: TcEvBinds -- This field is why we need an EvFun 537 -- constructor, and can't just use EvExpr 538 , et_body :: EvVar } 539 540 deriving Data.Data 541 542type EvExpr = CoreExpr 543 544-- An EvTerm is (usually) constructed by any of the constructors here 545-- and those more complicates ones who were moved to module TcEvTerm 546 547-- | Any sort of evidence Id, including coercions 548evId :: EvId -> EvExpr 549evId = Var 550 551-- coercion bindings 552-- See Note [Coercion evidence terms] 553evCoercion :: TcCoercion -> EvTerm 554evCoercion co = EvExpr (Coercion co) 555 556-- | d |> co 557evCast :: EvExpr -> TcCoercion -> EvTerm 558evCast et tc | isReflCo tc = EvExpr et 559 | otherwise = EvExpr (Cast et tc) 560 561-- Dictionary instance application 562evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvTerm 563evDFunApp df tys ets = EvExpr $ Var df `mkTyApps` tys `mkApps` ets 564 565evDataConApp :: DataCon -> [Type] -> [EvExpr] -> EvTerm 566evDataConApp dc tys ets = evDFunApp (dataConWrapId dc) tys ets 567 568-- Selector id plus the types at which it 569-- should be instantiated, used for HasField 570-- dictionaries; see Note [HasField instances] 571-- in TcInterface 572evSelector :: Id -> [Type] -> [EvExpr] -> EvExpr 573evSelector sel_id tys tms = Var sel_id `mkTyApps` tys `mkApps` tms 574 575-- Dictionary for (Typeable ty) 576evTypeable :: Type -> EvTypeable -> EvTerm 577evTypeable = EvTypeable 578 579-- | Instructions on how to make a 'Typeable' dictionary. 580-- See Note [Typeable evidence terms] 581data EvTypeable 582 = EvTypeableTyCon TyCon [EvTerm] 583 -- ^ Dictionary for @Typeable T@ where @T@ is a type constructor with all of 584 -- its kind variables saturated. The @[EvTerm]@ is @Typeable@ evidence for 585 -- the applied kinds.. 586 587 | EvTypeableTyApp EvTerm EvTerm 588 -- ^ Dictionary for @Typeable (s t)@, 589 -- given a dictionaries for @s@ and @t@. 590 591 | EvTypeableTrFun EvTerm EvTerm 592 -- ^ Dictionary for @Typeable (s -> t)@, 593 -- given a dictionaries for @s@ and @t@. 594 595 | EvTypeableTyLit EvTerm 596 -- ^ Dictionary for a type literal, 597 -- e.g. @Typeable "foo"@ or @Typeable 3@ 598 -- The 'EvTerm' is evidence of, e.g., @KnownNat 3@ 599 -- (see #10348) 600 deriving Data.Data 601 602-- | Evidence for @CallStack@ implicit parameters. 603data EvCallStack 604 -- See Note [Overview of implicit CallStacks] 605 = EvCsEmpty 606 | EvCsPushCall Name RealSrcSpan EvExpr 607 -- ^ @EvCsPushCall name loc stk@ represents a call to @name@, occurring at 608 -- @loc@, in a calling context @stk@. 609 deriving Data.Data 610 611{- 612Note [Typeable evidence terms] 613~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 614The EvTypeable data type looks isomorphic to Type, but the EvTerms 615inside can be EvIds. Eg 616 f :: forall a. Typeable a => a -> TypeRep 617 f x = typeRep (undefined :: Proxy [a]) 618Here for the (Typeable [a]) dictionary passed to typeRep we make 619evidence 620 dl :: Typeable [a] = EvTypeable [a] 621 (EvTypeableTyApp (EvTypeableTyCon []) (EvId d)) 622where 623 d :: Typable a 624is the lambda-bound dictionary passed into f. 625 626Note [Coercion evidence terms] 627~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 628A "coercion evidence term" takes one of these forms 629 co_tm ::= EvId v where v :: t1 ~# t2 630 | EvCoercion co 631 | EvCast co_tm co 632 633We do quite often need to get a TcCoercion from an EvTerm; see 634'evTermCoercion'. 635 636INVARIANT: The evidence for any constraint with type (t1 ~# t2) is 637a coercion evidence term. Consider for example 638 [G] d :: F Int a 639If we have 640 ax7 a :: F Int a ~ (a ~ Bool) 641then we do NOT generate the constraint 642 [G] (d |> ax7 a) :: a ~ Bool 643because that does not satisfy the invariant (d is not a coercion variable). 644Instead we make a binding 645 g1 :: a~Bool = g |> ax7 a 646and the constraint 647 [G] g1 :: a~Bool 648See #7238 and Note [Bind new Givens immediately] in Constraint 649 650Note [EvBinds/EvTerm] 651~~~~~~~~~~~~~~~~~~~~~ 652How evidence is created and updated. Bindings for dictionaries, 653and coercions and implicit parameters are carried around in TcEvBinds 654which during constraint generation and simplification is always of the 655form (TcEvBinds ref). After constraint simplification is finished it 656will be transformed to t an (EvBinds ev_bag). 657 658Evidence for coercions *SHOULD* be filled in using the TcEvBinds 659However, all EvVars that correspond to *wanted* coercion terms in 660an EvBind must be mutable variables so that they can be readily 661inlined (by zonking) after constraint simplification is finished. 662 663Conclusion: a new wanted coercion variable should be made mutable. 664[Notice though that evidence variables that bind coercion terms 665 from super classes will be "given" and hence rigid] 666 667 668Note [Overview of implicit CallStacks] 669~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 670(See https://gitlab.haskell.org/ghc/ghc/wikis/explicit-call-stack/implicit-locations) 671 672The goal of CallStack evidence terms is to reify locations 673in the program source as runtime values, without any support 674from the RTS. We accomplish this by assigning a special meaning 675to constraints of type GHC.Stack.Types.HasCallStack, an alias 676 677 type HasCallStack = (?callStack :: CallStack) 678 679Implicit parameters of type GHC.Stack.Types.CallStack (the name is not 680important) are solved in three steps: 681 6821. Occurrences of CallStack IPs are solved directly from the given IP, 683 just like a regular IP. For example, the occurrence of `?stk` in 684 685 error :: (?stk :: CallStack) => String -> a 686 error s = raise (ErrorCall (s ++ prettyCallStack ?stk)) 687 688 will be solved for the `?stk` in `error`s context as before. 689 6902. In a function call, instead of simply passing the given IP, we first 691 append the current call-site to it. For example, consider a 692 call to the callstack-aware `error` above. 693 694 undefined :: (?stk :: CallStack) => a 695 undefined = error "undefined!" 696 697 Here we want to take the given `?stk` and append the current 698 call-site, before passing it to `error`. In essence, we want to 699 rewrite `error "undefined!"` to 700 701 let ?stk = pushCallStack <error's location> ?stk 702 in error "undefined!" 703 704 We achieve this effect by emitting a NEW wanted 705 706 [W] d :: IP "stk" CallStack 707 708 from which we build the evidence term 709 710 EvCsPushCall "error" <error's location> (EvId d) 711 712 that we use to solve the call to `error`. The new wanted `d` will 713 then be solved per rule (1), ie as a regular IP. 714 715 (see TcInteract.interactDict) 716 7173. We default any insoluble CallStacks to the empty CallStack. Suppose 718 `undefined` did not request a CallStack, ie 719 720 undefinedNoStk :: a 721 undefinedNoStk = error "undefined!" 722 723 Under the usual IP rules, the new wanted from rule (2) would be 724 insoluble as there's no given IP from which to solve it, so we 725 would get an "unbound implicit parameter" error. 726 727 We don't ever want to emit an insoluble CallStack IP, so we add a 728 defaulting pass to default any remaining wanted CallStacks to the 729 empty CallStack with the evidence term 730 731 EvCsEmpty 732 733 (see TcSimplify.simpl_top and TcSimplify.defaultCallStacks) 734 735This provides a lightweight mechanism for building up call-stacks 736explicitly, but is notably limited by the fact that the stack will 737stop at the first function whose type does not include a CallStack IP. 738For example, using the above definition of `undefined`: 739 740 head :: [a] -> a 741 head [] = undefined 742 head (x:_) = x 743 744 g = head [] 745 746the resulting CallStack will include the call to `undefined` in `head` 747and the call to `error` in `undefined`, but *not* the call to `head` 748in `g`, because `head` did not explicitly request a CallStack. 749 750 751Important Details: 752- GHC should NEVER report an insoluble CallStack constraint. 753 754- GHC should NEVER infer a CallStack constraint unless one was requested 755 with a partial type signature (See TcType.pickQuantifiablePreds). 756 757- A CallStack (defined in GHC.Stack.Types) is a [(String, SrcLoc)], 758 where the String is the name of the binder that is used at the 759 SrcLoc. SrcLoc is also defined in GHC.Stack.Types and contains the 760 package/module/file name, as well as the full source-span. Both 761 CallStack and SrcLoc are kept abstract so only GHC can construct new 762 values. 763 764- We will automatically solve any wanted CallStack regardless of the 765 name of the IP, i.e. 766 767 f = show (?stk :: CallStack) 768 g = show (?loc :: CallStack) 769 770 are both valid. However, we will only push new SrcLocs onto existing 771 CallStacks when the IP names match, e.g. in 772 773 head :: (?loc :: CallStack) => [a] -> a 774 head [] = error (show (?stk :: CallStack)) 775 776 the printed CallStack will NOT include head's call-site. This reflects the 777 standard scoping rules of implicit-parameters. 778 779- An EvCallStack term desugars to a CoreExpr of type `IP "some str" CallStack`. 780 The desugarer will need to unwrap the IP newtype before pushing a new 781 call-site onto a given stack (See DsBinds.dsEvCallStack) 782 783- When we emit a new wanted CallStack from rule (2) we set its origin to 784 `IPOccOrigin ip_name` instead of the original `OccurrenceOf func` 785 (see TcInteract.interactDict). 786 787 This is a bit shady, but is how we ensure that the new wanted is 788 solved like a regular IP. 789 790-} 791 792mkEvCast :: EvExpr -> TcCoercion -> EvTerm 793mkEvCast ev lco 794 | ASSERT2( tcCoercionRole lco == Representational 795 , (vcat [text "Coercion of wrong role passed to mkEvCast:", ppr ev, ppr lco])) 796 isTcReflCo lco = EvExpr ev 797 | otherwise = evCast ev lco 798 799 800mkEvScSelectors -- Assume class (..., D ty, ...) => C a b 801 :: Class -> [TcType] -- C ty1 ty2 802 -> [(TcPredType, -- D ty[ty1/a,ty2/b] 803 EvExpr) -- :: C ty1 ty2 -> D ty[ty1/a,ty2/b] 804 ] 805mkEvScSelectors cls tys 806 = zipWith mk_pr (immSuperClasses cls tys) [0..] 807 where 808 mk_pr pred i = (pred, Var sc_sel_id `mkTyApps` tys) 809 where 810 sc_sel_id = classSCSelId cls i -- Zero-indexed 811 812emptyTcEvBinds :: TcEvBinds 813emptyTcEvBinds = EvBinds emptyBag 814 815isEmptyTcEvBinds :: TcEvBinds -> Bool 816isEmptyTcEvBinds (EvBinds b) = isEmptyBag b 817isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds" 818 819evTermCoercion_maybe :: EvTerm -> Maybe TcCoercion 820-- Applied only to EvTerms of type (s~t) 821-- See Note [Coercion evidence terms] 822evTermCoercion_maybe ev_term 823 | EvExpr e <- ev_term = go e 824 | otherwise = Nothing 825 where 826 go :: EvExpr -> Maybe TcCoercion 827 go (Var v) = return (mkCoVarCo v) 828 go (Coercion co) = return co 829 go (Cast tm co) = do { co' <- go tm 830 ; return (mkCoCast co' co) } 831 go _ = Nothing 832 833evTermCoercion :: EvTerm -> TcCoercion 834evTermCoercion tm = case evTermCoercion_maybe tm of 835 Just co -> co 836 Nothing -> pprPanic "evTermCoercion" (ppr tm) 837 838 839{- ********************************************************************* 840* * 841 Free variables 842* * 843********************************************************************* -} 844 845findNeededEvVars :: EvBindMap -> VarSet -> VarSet 846-- Find all the Given evidence needed by seeds, 847-- looking transitively through binds 848findNeededEvVars ev_binds seeds 849 = transCloVarSet also_needs seeds 850 where 851 also_needs :: VarSet -> VarSet 852 also_needs needs = nonDetFoldUniqSet add emptyVarSet needs 853 -- It's OK to use nonDetFoldUFM here because we immediately 854 -- forget about the ordering by creating a set 855 856 add :: Var -> VarSet -> VarSet 857 add v needs 858 | Just ev_bind <- lookupEvBind ev_binds v 859 , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind 860 , is_given 861 = evVarsOfTerm rhs `unionVarSet` needs 862 | otherwise 863 = needs 864 865evVarsOfTerm :: EvTerm -> VarSet 866evVarsOfTerm (EvExpr e) = exprSomeFreeVars isEvVar e 867evVarsOfTerm (EvTypeable _ ev) = evVarsOfTypeable ev 868evVarsOfTerm (EvFun {}) = emptyVarSet -- See Note [Free vars of EvFun] 869 870evVarsOfTerms :: [EvTerm] -> VarSet 871evVarsOfTerms = mapUnionVarSet evVarsOfTerm 872 873evVarsOfTypeable :: EvTypeable -> VarSet 874evVarsOfTypeable ev = 875 case ev of 876 EvTypeableTyCon _ e -> mapUnionVarSet evVarsOfTerm e 877 EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2] 878 EvTypeableTrFun e1 e2 -> evVarsOfTerms [e1,e2] 879 EvTypeableTyLit e -> evVarsOfTerm e 880 881 882{- Note [Free vars of EvFun] 883~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 884Finding the free vars of an EvFun is made tricky by the fact the 885bindings et_binds may be a mutable variable. Fortunately, we 886can just squeeze by. Here's how. 887 888* evVarsOfTerm is used only by TcSimplify.neededEvVars. 889* Each EvBindsVar in an et_binds field of an EvFun is /also/ in the 890 ic_binds field of an Implication 891* So we can track usage via the processing for that implication, 892 (see Note [Tracking redundant constraints] in TcSimplify). 893 We can ignore usage from the EvFun altogether. 894 895************************************************************************ 896* * 897 Pretty printing 898* * 899************************************************************************ 900-} 901 902instance Outputable HsWrapper where 903 ppr co_fn = pprHsWrapper co_fn (no_parens (text "<>")) 904 905pprHsWrapper :: HsWrapper -> (Bool -> SDoc) -> SDoc 906-- With -fprint-typechecker-elaboration, print the wrapper 907-- otherwise just print what's inside 908-- The pp_thing_inside function takes Bool to say whether 909-- it's in a position that needs parens for a non-atomic thing 910pprHsWrapper wrap pp_thing_inside 911 = sdocWithDynFlags $ \ dflags -> 912 if gopt Opt_PrintTypecheckerElaboration dflags 913 then help pp_thing_inside wrap False 914 else pp_thing_inside False 915 where 916 help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc 917 -- True <=> appears in function application position 918 -- False <=> appears as body of let or lambda 919 help it WpHole = it 920 help it (WpCompose f1 f2) = help (help it f2) f1 921 help it (WpFun f1 f2 t1 _) = add_parens $ text "\\(x" <> dcolon <> ppr t1 <> text ")." <+> 922 help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False 923 help it (WpCast co) = add_parens $ sep [it False, nest 2 (text "|>" 924 <+> pprParendCo co)] 925 help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)] 926 help it (WpTyApp ty) = no_parens $ sep [it True, text "@" <+> pprParendType ty] 927 help it (WpEvLam id) = add_parens $ sep [ text "\\" <> pprLamBndr id <> dot, it False] 928 help it (WpTyLam tv) = add_parens $ sep [text "/\\" <> pprLamBndr tv <> dot, it False] 929 help it (WpLet binds) = add_parens $ sep [text "let" <+> braces (ppr binds), it False] 930 931pprLamBndr :: Id -> SDoc 932pprLamBndr v = pprBndr LambdaBind v 933 934add_parens, no_parens :: SDoc -> Bool -> SDoc 935add_parens d True = parens d 936add_parens d False = d 937no_parens d _ = d 938 939instance Outputable TcEvBinds where 940 ppr (TcEvBinds v) = ppr v 941 ppr (EvBinds bs) = text "EvBinds" <> braces (vcat (map ppr (bagToList bs))) 942 943instance Outputable EvBindsVar where 944 ppr (EvBindsVar { ebv_uniq = u }) 945 = text "EvBindsVar" <> angleBrackets (ppr u) 946 ppr (CoEvBindsVar { ebv_uniq = u }) 947 = text "CoEvBindsVar" <> angleBrackets (ppr u) 948 949instance Uniquable EvBindsVar where 950 getUnique = ebv_uniq 951 952instance Outputable EvBind where 953 ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given }) 954 = sep [ pp_gw <+> ppr v 955 , nest 2 $ equals <+> ppr e ] 956 where 957 pp_gw = brackets (if is_given then char 'G' else char 'W') 958 -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing 959 960instance Outputable EvTerm where 961 ppr (EvExpr e) = ppr e 962 ppr (EvTypeable ty ev) = ppr ev <+> dcolon <+> text "Typeable" <+> ppr ty 963 ppr (EvFun { et_tvs = tvs, et_given = gs, et_binds = bs, et_body = w }) 964 = hang (text "\\" <+> sep (map pprLamBndr (tvs ++ gs)) <+> arrow) 965 2 (ppr bs $$ ppr w) -- Not very pretty 966 967instance Outputable EvCallStack where 968 ppr EvCsEmpty 969 = text "[]" 970 ppr (EvCsPushCall name loc tm) 971 = ppr (name,loc) <+> text ":" <+> ppr tm 972 973instance Outputable EvTypeable where 974 ppr (EvTypeableTyCon ts _) = text "TyCon" <+> ppr ts 975 ppr (EvTypeableTyApp t1 t2) = parens (ppr t1 <+> ppr t2) 976 ppr (EvTypeableTrFun t1 t2) = parens (ppr t1 <+> arrow <+> ppr t2) 977 ppr (EvTypeableTyLit t1) = text "TyLit" <> ppr t1 978 979 980---------------------------------------------------------------------- 981-- Helper functions for dealing with IP newtype-dictionaries 982---------------------------------------------------------------------- 983 984-- | Create a 'Coercion' that unwraps an implicit-parameter or 985-- overloaded-label dictionary to expose the underlying value. We 986-- expect the 'Type' to have the form `IP sym ty` or `IsLabel sym ty`, 987-- and return a 'Coercion' `co :: IP sym ty ~ ty` or 988-- `co :: IsLabel sym ty ~ Proxy# sym -> ty`. See also 989-- Note [Type-checking overloaded labels] in TcExpr. 990unwrapIP :: Type -> CoercionR 991unwrapIP ty = 992 case unwrapNewTyCon_maybe tc of 993 Just (_,_,ax) -> mkUnbranchedAxInstCo Representational ax tys [] 994 Nothing -> pprPanic "unwrapIP" $ 995 text "The dictionary for" <+> quotes (ppr tc) 996 <+> text "is not a newtype!" 997 where 998 (tc, tys) = splitTyConApp ty 999 1000-- | Create a 'Coercion' that wraps a value in an implicit-parameter 1001-- dictionary. See 'unwrapIP'. 1002wrapIP :: Type -> CoercionR 1003wrapIP ty = mkSymCo (unwrapIP ty) 1004