compiler/typecheck/TcEvidence.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 %
   4
   5 \begin{code}
   6 module TcEvidence (
   7
   8   -- HsWrapper
   9   HsWrapper(..),
  10   (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet,
  11   idHsWrapper, isIdHsWrapper, pprHsWrapper,
  12
  13   -- Evidence bindin
  14   TcEvBinds(..), EvBindsVar(..),
  15   EvBindMap(..), emptyEvBindMap, extendEvBinds, lookupEvBind, evBindMapBinds,
  16
  17   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds,
  18
  19   EvTerm(..), mkEvCast, evVarsOfTerm, mkEvKindCast,
  20   EvLit(..), evTermCoercion,
  21
  22   -- TcCoercion
  23   TcCoercion(..),
  24   mkTcReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
  25   mkTcAxInstCo, mkTcForAllCo, mkTcForAllCos,
  26   mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcInstCos,
  27   tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo,
  28   isTcReflCo, isTcReflCo_maybe, getTcCoVar_maybe,
  29   liftTcCoSubstWith
  30
  31   ) where
  32 #include "HsVersions.h"
  33
  34 import Var
  35
  36 import PprCore ()   -- Instance OutputableBndr TyVar
  37 import TypeRep  -- Knows type representation
  38 import TcType
  39 import Type( tyConAppArgN, getEqPredTys_maybe, tyConAppTyCon_maybe, getEqPredTys )
  40 import TysPrim( funTyCon )
  41 import TyCon
  42 import PrelNames
  43 import VarEnv
  44 import VarSet
  45 import Name
  46
  47 import Util
  48 import Bag
  49 import Pair
  50 import Control.Applicative
  51 import Data.Traversable (traverse, sequenceA)
  52 import qualified Data.Data as Data
  53 import Outputable
  54 import FastString
  55 import Data.IORef( IORef )
  56 \end{code}
  57
  58
  59 Note [TcCoercions]
  60 ~~~~~~~~~~~~~~~~~~
  61 | LCoercions are a hack used by the typechecker. Normally,
  62 Coercions have free variables of type (a ~# b): we call these
  63 CoVars. However, the type checker passes around equality evidence
  64 (boxed up) at type (a ~ b).
  65
  66 An LCoercion is simply a Coercion whose free variables have the
  67 boxed type (a ~ b). After we are done with typechecking the
  68 desugarer finds the free variables, unboxes them, and creates a
  69 resulting real Coercion with kosher free variables.
  70
  71 We can use most of the Coercion "smart constructors" to build LCoercions. However,
  72 mkCoVarCo will not work! The equivalent is mkTcCoVarCo.
  73
  74 The data type is similar to Coercion.Coercion, with the following
  75 differences
  76   * Most important, TcLetCo adds let-bindings for coercions.
  77     This is what lets us unify two for-all types and generate
  78     equality constraints underneath
  79
  80   * The kind of a TcCoercion is  t1 ~  t2
  81              of a Coercion   is  t1 ~# t2
  82
  83   * TcAxiomInstCo takes Types, not Coecions as arguments;
  84     the generality is required only in the Simplifier
  85
  86   * UnsafeCo aren't required
  87
  88   * Reprsentation invariants are weaker:
  89      - we are allowed to have type synonyms in TcTyConAppCo
  90      - the first arg of a TcAppCo can be a TcTyConAppCo
  91     Reason: they'll get established when we desugar to Coercion
  92
  93 \begin{code}
  94 data TcCoercion
  95   = TcRefl TcType
  96   | TcTyConAppCo TyCon [TcCoercion]
  97   | TcAppCo TcCoercion TcCoercion
  98   | TcForAllCo TyVar TcCoercion
  99   | TcInstCo TcCoercion TcType
 100   | TcCoVarCo EqVar
 101   | TcAxiomInstCo CoAxiom [TcType]
 102   | TcSymCo TcCoercion
 103   | TcTransCo TcCoercion TcCoercion
 104   | TcNthCo Int TcCoercion
 105   | TcCastCo TcCoercion TcCoercion     -- co1 |> co2
 106   | TcLetCo TcEvBinds TcCoercion
 107   deriving (Data.Data, Data.Typeable)
 108
 109 isEqVar :: Var -> Bool
 110 -- Is lifted coercion variable (only!)
 111 isEqVar v = case tyConAppTyCon_maybe (varType v) of
 112                Just tc -> tc `hasKey` eqTyConKey
 113                Nothing -> False
 114
 115 isTcReflCo_maybe :: TcCoercion -> Maybe TcType
 116 isTcReflCo_maybe (TcRefl ty) = Just ty
 117 isTcReflCo_maybe _             = Nothing
 118
 119 isTcReflCo :: TcCoercion -> Bool
 120 isTcReflCo (TcRefl {}) = True
 121 isTcReflCo _           = False
 122
 123 getTcCoVar_maybe :: TcCoercion -> Maybe CoVar
 124 getTcCoVar_maybe (TcCoVarCo v) = Just v
 125 getTcCoVar_maybe _             = Nothing
 126
 127 mkTcReflCo :: TcType -> TcCoercion
 128 mkTcReflCo = TcRefl
 129
 130 mkTcFunCo :: TcCoercion -> TcCoercion -> TcCoercion
 131 mkTcFunCo co1 co2 = mkTcTyConAppCo funTyCon [co1, co2]
 132
 133 mkTcTyConAppCo :: TyCon -> [TcCoercion] -> TcCoercion
 134 mkTcTyConAppCo tc cos   -- No need to expand type synonyms
 135                         -- See Note [TcCoercions]
 136   | Just tys <- traverse isTcReflCo_maybe cos
 137   = TcRefl (mkTyConApp tc tys)    -- See Note [Refl invariant]
 138
 139   | otherwise = TcTyConAppCo tc cos
 140
 141 mkTcAxInstCo :: CoAxiom -> [TcType] -> TcCoercion
 142 mkTcAxInstCo ax tys
 143   | arity == n_tys = TcAxiomInstCo ax tys
 144   | otherwise      = ASSERT( arity < n_tys )
 145                      foldl TcAppCo (TcAxiomInstCo ax (take arity tys))
 146                                    (map TcRefl (drop arity tys))
 147   where
 148     n_tys = length tys
 149     arity = coAxiomArity ax
 150
 151 mkTcAppCo :: TcCoercion -> TcCoercion -> TcCoercion
 152 -- No need to deal with TyConApp on the left; see Note [TcCoercions]
 153 mkTcAppCo (TcRefl ty1) (TcRefl ty2)     = TcRefl (mkAppTy ty1 ty2)
 154 mkTcAppCo co1 co2                       = TcAppCo co1 co2
 155
 156 mkTcSymCo :: TcCoercion -> TcCoercion
 157 mkTcSymCo co@(TcRefl {})  = co
 158 mkTcSymCo    (TcSymCo co) = co
 159 mkTcSymCo co              = TcSymCo co
 160
 161 mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion
 162 mkTcTransCo (TcRefl _) co = co
 163 mkTcTransCo co (TcRefl _) = co
 164 mkTcTransCo co1 co2       = TcTransCo co1 co2
 165
 166 mkTcNthCo :: Int -> TcCoercion -> TcCoercion
 167 mkTcNthCo n (TcRefl ty) = TcRefl (tyConAppArgN n ty)
 168 mkTcNthCo n co          = TcNthCo n co
 169
 170 mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion
 171 mkTcAppCos co1 tys = foldl mkTcAppCo co1 tys
 172
 173 mkTcForAllCo :: Var -> TcCoercion -> TcCoercion
 174 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
 175 mkTcForAllCo tv (TcRefl ty) = ASSERT( isTyVar tv ) TcRefl (mkForAllTy tv ty)
 176 mkTcForAllCo tv  co         = ASSERT( isTyVar tv ) TcForAllCo tv co
 177
 178 mkTcForAllCos :: [Var] -> TcCoercion -> TcCoercion
 179 mkTcForAllCos tvs (TcRefl ty) = ASSERT( all isTyVar tvs ) TcRefl (mkForAllTys tvs ty)
 180 mkTcForAllCos tvs co          = ASSERT( all isTyVar tvs ) foldr TcForAllCo co tvs
 181
 182 mkTcInstCos :: TcCoercion -> [TcType] -> TcCoercion
 183 mkTcInstCos (TcRefl ty) tys = TcRefl (applyTys ty tys)
 184 mkTcInstCos co tys          = foldl TcInstCo co tys
 185
 186 mkTcCoVarCo :: EqVar -> TcCoercion
 187 -- ipv :: s ~ t  (the boxed equality type)
 188 mkTcCoVarCo ipv
 189   | ty1 `eqType` ty2 = TcRefl ty1
 190   | otherwise        = TcCoVarCo ipv
 191   where
 192     (ty1, ty2) = case getEqPredTys_maybe (varType ipv) of
 193         Nothing  -> pprPanic "mkCoVarLCo" (ppr ipv)
 194         Just tys -> tys
 195 \end{code}
 196
 197 \begin{code}
 198 tcCoercionKind :: TcCoercion -> Pair Type
 199 tcCoercionKind co = go co
 200   where
 201     go (TcRefl ty)            = Pair ty ty
 202     go (TcLetCo _ co)         = go co
 203     go (TcCastCo _ co)        = case getEqPredTys (pSnd (go co)) of
 204                                    (ty1,ty2) -> Pair ty1 ty2
 205     go (TcTyConAppCo tc cos)  = mkTyConApp tc <$> (sequenceA $ map go cos)
 206     go (TcAppCo co1 co2)      = mkAppTy <$> go co1 <*> go co2
 207     go (TcForAllCo tv co)     = mkForAllTy tv <$> go co
 208     go (TcInstCo co ty)       = go_inst co [ty]
 209     go (TcCoVarCo cv)         = eqVarKind cv
 210     go (TcAxiomInstCo ax tys) = Pair (substTyWith (co_ax_tvs ax) tys (co_ax_lhs ax))
 211                                      (substTyWith (co_ax_tvs ax) tys (co_ax_rhs ax))
 212     go (TcSymCo co)           = swap (go co)
 213     go (TcTransCo co1 co2)    = Pair (pFst (go co1)) (pSnd (go co2))
 214     go (TcNthCo d co)         = tyConAppArgN d <$> go co
 215
 216     -- c.f. Coercion.coercionKind
 217     go_inst (TcInstCo co ty) tys = go_inst co (ty:tys)
 218     go_inst co               tys = (`applyTys` tys) <$> go co
 219
 220 eqVarKind :: EqVar -> Pair Type
 221 eqVarKind cv
 222  | Just (tc, [_kind,ty1,ty2]) <- tcSplitTyConApp_maybe (varType cv)
 223  = ASSERT (tc `hasKey` eqTyConKey)
 224    Pair ty1 ty2
 225  | otherwise = pprPanic "eqVarKind, non coercion variable" (ppr cv <+> dcolon <+> ppr (varType cv))
 226
 227 coVarsOfTcCo :: TcCoercion -> VarSet
 228 -- Only works on *zonked* coercions, because of TcLetCo
 229 coVarsOfTcCo tc_co
 230   = go tc_co
 231   where
 232     go (TcRefl _)                = emptyVarSet
 233     go (TcTyConAppCo _ cos)      = foldr (unionVarSet . go) emptyVarSet cos
 234     go (TcAppCo co1 co2)         = go co1 `unionVarSet` go co2
 235     go (TcCastCo co1 co2)        = go co1 `unionVarSet` go co2
 236     go (TcForAllCo _ co)         = go co
 237     go (TcInstCo co _)           = go co
 238     go (TcCoVarCo v)             = unitVarSet v
 239     go (TcAxiomInstCo {})        = emptyVarSet
 240     go (TcSymCo co)              = go co
 241     go (TcTransCo co1 co2)       = go co1 `unionVarSet` go co2
 242     go (TcNthCo _ co)            = go co
 243     go (TcLetCo (EvBinds bs) co) = foldrBag (unionVarSet . go_bind) (go co) bs
 244                                    `minusVarSet` get_bndrs bs
 245     go (TcLetCo {}) = pprPanic "coVarsOfTcCo called on non-zonked TcCoercion" (ppr tc_co)
 246
 247     -- We expect only coercion bindings
 248     go_bind :: EvBind -> VarSet
 249     go_bind (EvBind _ (EvCoercion co)) = go co
 250     go_bind (EvBind _ (EvId v))        = unitVarSet v
 251     go_bind other = pprPanic "coVarsOfTcCo:Bind" (ppr other)
 252
 253     get_bndrs :: Bag EvBind -> VarSet
 254     get_bndrs = foldrBag (\ (EvBind b _) bs -> extendVarSet bs b) emptyVarSet
 255
 256 liftTcCoSubstWith :: [TyVar] -> [TcCoercion] -> TcType -> TcCoercion
 257 -- This version can ignore capture; the free varialbes of the
 258 -- TcCoerion are all fresh.  Result is mush simpler code
 259 liftTcCoSubstWith tvs cos ty
 260   = ASSERT( equalLength tvs cos )
 261     go ty
 262   where
 263     env = zipVarEnv tvs cos
 264
 265     go ty@(TyVarTy tv)   = case lookupVarEnv env tv of
 266                              Just co -> co
 267                              Nothing -> mkTcReflCo ty
 268     go (AppTy t1 t2)     = mkTcAppCo (go t1) (go t2)
 269     go (TyConApp tc tys) = mkTcTyConAppCo tc (map go tys)
 270     go ty@(LitTy {})     = mkTcReflCo ty
 271     go (ForAllTy tv ty)  = mkTcForAllCo tv (go ty)
 272     go (FunTy t1 t2)     = mkTcFunCo (go t1) (go t2)
 273 \end{code}
 274
 275 Pretty printing
 276
 277 \begin{code}
 278 instance Outputable TcCoercion where
 279   ppr = pprTcCo
 280
 281 pprTcCo, pprParendTcCo :: TcCoercion -> SDoc
 282 pprTcCo       co = ppr_co TopPrec   co
 283 pprParendTcCo co = ppr_co TyConPrec co
 284
 285 ppr_co :: Prec -> TcCoercion -> SDoc
 286 ppr_co _ (TcRefl ty) = angleBrackets (ppr ty)
 287
 288 ppr_co p co@(TcTyConAppCo tc [_,_])
 289   | tc `hasKey` funTyConKey = ppr_fun_co p co
 290
 291 ppr_co p (TcTyConAppCo tc cos)   = pprTcApp   p ppr_co tc cos
 292 ppr_co p (TcLetCo bs co)         = maybeParen p TopPrec $
 293                                    sep [ptext (sLit "let") <+> braces (ppr bs), ppr co]
 294 ppr_co p (TcAppCo co1 co2)       = maybeParen p TyConPrec $
 295                                    pprTcCo co1 <+> ppr_co TyConPrec co2
 296 ppr_co p (TcCastCo co1 co2)      = maybeParen p FunPrec $
 297                                    ppr_co FunPrec co1 <+> ptext (sLit "|>") <+> ppr_co FunPrec co2
 298 ppr_co p co@(TcForAllCo {})      = ppr_forall_co p co
 299 ppr_co p (TcInstCo co ty)        = maybeParen p TyConPrec $
 300                                    pprParendTcCo co <> ptext (sLit "@") <> pprType ty
 301
 302 ppr_co _ (TcCoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)
 303 ppr_co p (TcAxiomInstCo con cos) = pprTypeNameApp p ppr_type (getName con) cos
 304
 305 ppr_co p (TcTransCo co1 co2) = maybeParen p FunPrec $
 306                                ppr_co FunPrec co1
 307                                <+> ptext (sLit ";")
 308                                <+> ppr_co FunPrec co2
 309 ppr_co p (TcSymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co]
 310 ppr_co p (TcNthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co]
 311
 312 ppr_fun_co :: Prec -> TcCoercion -> SDoc
 313 ppr_fun_co p co = pprArrowChain p (split co)
 314   where
 315     split :: TcCoercion -> [SDoc]
 316     split (TcTyConAppCo f [arg,res])
 317       | f `hasKey` funTyConKey
 318       = ppr_co FunPrec arg : split res
 319     split co = [ppr_co TopPrec co]
 320
 321 ppr_forall_co :: Prec -> TcCoercion -> SDoc
 322 ppr_forall_co p ty
 323   = maybeParen p FunPrec $
 324     sep [pprForAll tvs, ppr_co TopPrec rho]
 325   where
 326     (tvs,  rho) = split1 [] ty
 327     split1 tvs (TcForAllCo tv ty) = split1 (tv:tvs) ty
 328     split1 tvs ty                 = (reverse tvs, ty)
 329 \end{code}
 330
 331 %************************************************************************
 332 %*                                                                      *
 333                   HsWrapper
 334 %*                                                                      *
 335 %************************************************************************
 336
 337 \begin{code}
 338 data HsWrapper
 339   = WpHole                      -- The identity coercion
 340
 341   | WpCompose HsWrapper HsWrapper
 342        -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
 343        --
 344        -- Hence  (\a. []) `WpCompose` (\b. []) = (\a b. [])
 345        -- But    ([] a)   `WpCompose` ([] b)   = ([] b a)
 346
 347   | WpCast TcCoercion         -- A cast:  [] `cast` co
 348                               -- Guaranteed not the identity coercion
 349
 350         -- Evidence abstraction and application
 351         -- (both dictionaries and coercions)
 352   | WpEvLam EvVar               -- \d. []       the 'd' is an evidence variable
 353   | WpEvApp EvTerm              -- [] d         the 'd' is evidence for a constraint
 354
 355         -- Kind and Type abstraction and application
 356   | WpTyLam TyVar       -- \a. []  the 'a' is a type/kind variable (not coercion var)
 357   | WpTyApp KindOrType  -- [] t    the 't' is a type (not coercion)
 358
 359
 360   | WpLet TcEvBinds             -- Non-empty (or possibly non-empty) evidence bindings,
 361                                 -- so that the identity coercion is always exactly WpHole
 362   deriving (Data.Data, Data.Typeable)
 363
 364
 365 (<.>) :: HsWrapper -> HsWrapper -> HsWrapper
 366 WpHole <.> c = c
 367 c <.> WpHole = c
 368 c1 <.> c2    = c1 `WpCompose` c2
 369
 370 mkWpTyApps :: [Type] -> HsWrapper
 371 mkWpTyApps tys = mk_co_app_fn WpTyApp tys
 372
 373 mkWpEvApps :: [EvTerm] -> HsWrapper
 374 mkWpEvApps args = mk_co_app_fn WpEvApp args
 375
 376 mkWpEvVarApps :: [EvVar] -> HsWrapper
 377 mkWpEvVarApps vs = mkWpEvApps (map EvId vs)
 378
 379 mkWpTyLams :: [TyVar] -> HsWrapper
 380 mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
 381
 382 mkWpLams :: [Var] -> HsWrapper
 383 mkWpLams ids = mk_co_lam_fn WpEvLam ids
 384
 385 mkWpLet :: TcEvBinds -> HsWrapper
 386 -- This no-op is a quite a common case
 387 mkWpLet (EvBinds b) | isEmptyBag b = WpHole
 388 mkWpLet ev_binds                   = WpLet ev_binds
 389
 390 mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
 391 mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as
 392
 393 mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
 394 -- For applications, the *first* argument must
 395 -- come *last* in the composition sequence
 396 mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as
 397
 398 idHsWrapper :: HsWrapper
 399 idHsWrapper = WpHole
 400
 401 isIdHsWrapper :: HsWrapper -> Bool
 402 isIdHsWrapper WpHole = True
 403 isIdHsWrapper _      = False
 404 \end{code}
 405
 406
 407 %************************************************************************
 408 %*                                                                      *
 409                   Evidence bindings
 410 %*                                                                      *
 411 %************************************************************************
 412
 413 \begin{code}
 414 data TcEvBinds
 415   = TcEvBinds           -- Mutable evidence bindings
 416        EvBindsVar       -- Mutable because they are updated "later"
 417                         --    when an implication constraint is solved
 418
 419   | EvBinds             -- Immutable after zonking
 420        (Bag EvBind)
 421
 422   deriving( Data.Typeable )
 423
 424 data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique
 425      -- The Unique is only for debug printing
 426
 427 instance Data.Data TcEvBinds where
 428   -- Placeholder; we can't travers into TcEvBinds
 429   toConstr _   = abstractConstr "TcEvBinds"
 430   gunfold _ _  = error "gunfold"
 431   dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
 432
 433 -----------------
 434 newtype EvBindMap
 435   = EvBindMap {
 436        ev_bind_varenv :: VarEnv EvBind
 437     }       -- Map from evidence variables to evidence terms
 438
 439 emptyEvBindMap :: EvBindMap
 440 emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyVarEnv }
 441
 442 extendEvBinds :: EvBindMap -> EvVar -> EvTerm -> EvBindMap
 443 extendEvBinds bs v t
 444   = EvBindMap { ev_bind_varenv = extendVarEnv (ev_bind_varenv bs) v (EvBind v t) }
 445
 446 lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
 447 lookupEvBind bs = lookupVarEnv (ev_bind_varenv bs)
 448
 449 evBindMapBinds :: EvBindMap -> Bag EvBind
 450 evBindMapBinds bs
 451   = foldVarEnv consBag emptyBag (ev_bind_varenv bs)
 452
 453 -----------------
 454 -- All evidence is bound by EvBinds; no side effects
 455 data EvBind = EvBind EvVar EvTerm
 456
 457 data EvTerm
 458   = EvId EvId                    -- Any sort of evidence Id, including coercions
 459
 460   | EvCoercion TcCoercion        -- (Boxed) coercion bindings
 461                                  -- See Note [Coercion evidence terms]
 462
 463   | EvCast EvTerm TcCoercion     -- d |> co
 464
 465   | EvDFunApp DFunId             -- Dictionary instance application
 466        [Type] [EvTerm]
 467
 468   | EvTupleSel EvTerm  Int       -- n'th component of the tuple, 0-indexed
 469
 470   | EvTupleMk [EvTerm]           -- tuple built from this stuff
 471
 472   | EvDelayedError Type FastString  -- Used with Opt_DeferTypeErrors
 473                                -- See Note [Deferring coercion errors to runtime]
 474                                -- in TcSimplify
 475
 476   | EvSuperClass EvTerm Int      -- n'th superclass. Used for both equalities and
 477                                  -- dictionaries, even though the former have no
 478                                  -- selector Id.  We count up from _0_
 479
 480   | EvKindCast EvTerm TcCoercion  -- See Note [EvKindCast]
 481
 482   | EvLit EvLit                  -- Dictionary for class "SingI" for type lits.
 483                                  -- Note [EvLit]
 484
 485   deriving( Data.Data, Data.Typeable)
 486
 487
 488 data EvLit
 489   = EvNum Integer
 490   | EvStr FastString
 491     deriving( Data.Data, Data.Typeable)
 492
 493 \end{code}
 494
 495 Note [Coecion evidence terms]
 496 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 497 Notice that a coercion variable (v :: t1 ~ t2) can be represented as an EvTerm
 498 in two different ways:
 499    EvId v
 500    EvCoercion (TcCoVarCo v)
 501
 502 An alternative would be
 503
 504 * To establish the invariant that coercions are represented only
 505    by EvCoercion
 506
 507 * To maintain the invariant by smart constructors.  Eg
 508      mkEvCast (EvCoercion c1) c2 = EvCoercion (TcCastCo c1 c2)
 509      mkEvCast t c = EvCast t c
 510
 511 We do quite often need to get a TcCoercion from an EvTerm; see
 512 'evTermCoercion'.  Notice that as well as EvId and EvCoercion it may see
 513 an EvCast.
 514
 515 I don't think it matters much... but maybe we'll find a good reason to
 516 do one or the other.
 517
 518 Note [EvKindCast]
 519 ~~~~~~~~~~~~~~~~~
 520 EvKindCast g kco is produced when we have a constraint (g : s1 ~ s2)
 521 but the kinds of s1 and s2 (k1 and k2 respectively) don't match but
 522 are rather equal by a coercion. You may think that this coercion will
 523 always turn out to be ReflCo, so why is this needed? Because sometimes
 524 we will want to defer kind errors until the runtime and in these cases
 525 that coercion will be an 'error' term, which we want to evaluate rather
 526 than silently forget about!
 527
 528 The relevant (and only) place where such a coercion is produced in
 529 the simplifier is in TcCanonical.emitKindConstraint.
 530
 531 Note [EvBinds/EvTerm]
 532 ~~~~~~~~~~~~~~~~~~~~~
 533 How evidence is created and updated. Bindings for dictionaries,
 534 and coercions and implicit parameters are carried around in TcEvBinds
 535 which during constraint generation and simplification is always of the
 536 form (TcEvBinds ref). After constraint simplification is finished it
 537 will be transformed to t an (EvBinds ev_bag).
 538
 539 Evidence for coercions *SHOULD* be filled in using the TcEvBinds
 540 However, all EvVars that correspond to *wanted* coercion terms in
 541 an EvBind must be mutable variables so that they can be readily
 542 inlined (by zonking) after constraint simplification is finished.
 543
 544 Conclusion: a new wanted coercion variable should be made mutable.
 545 [Notice though that evidence variables that bind coercion terms
 546  from super classes will be "given" and hence rigid]
 547
 548
 549 Note [EvLit]
 550 ~~~~~~~~~~~~
 551 A part of the type-level literals implementation is the class "SingI",
 552 which provides a "smart" constructor for defining singleton values.
 553
 554 newtype Sing n = Sing (SingRep n)
 555
 556 class SingI n where
 557   sing :: Sing n
 558
 559 type family SingRep a
 560 type instance SingRep (a :: Nat)    = Integer
 561 type instance SingRep (a :: Symbol) = String
 562
 563 Conceptually, this class has infinitely many instances:
 564
 565 instance Sing 0       where sing = Sing 0
 566 instance Sing 1       where sing = Sing 1
 567 instance Sing 2       where sing = Sing 2
 568 instance Sing "hello" where sing = Sing "hello"
 569 ...
 570
 571 In practice, we solve "SingI" predicates in the type-checker because we can't
 572 have infinately many instances.  The evidence (aka "dictionary")
 573 for "SingI (n :: Nat)" is of the form "EvLit (EvNum n)".
 574
 575 We make the following assumptions about dictionaries in GHC:
 576   1. The "dictionary" for classes with a single method---like SingI---is
 577      a newtype for the type of the method, so using a evidence amounts
 578      to a coercion, and
 579   2. Newtypes use the same representation as their definition types.
 580
 581 So, the evidence for "SingI" is just a value of the representation type,
 582 wrapped in two newtype constructors: one to make it into a "Sing" value,
 583 and another to make it into "SingI" evidence.
 584
 585
 586 \begin{code}
 587 mkEvCast :: EvTerm -> TcCoercion -> EvTerm
 588 mkEvCast ev lco
 589   | isTcReflCo lco = ev
 590   | otherwise      = EvCast ev lco
 591
 592 mkEvKindCast :: EvTerm -> TcCoercion -> EvTerm
 593 mkEvKindCast ev lco
 594   | isTcReflCo lco = ev
 595   | otherwise      = EvKindCast ev lco
 596
 597 emptyTcEvBinds :: TcEvBinds
 598 emptyTcEvBinds = EvBinds emptyBag
 599
 600 isEmptyTcEvBinds :: TcEvBinds -> Bool
 601 isEmptyTcEvBinds (EvBinds b)    = isEmptyBag b
 602 isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
 603
 604
 605 evTermCoercion :: EvTerm -> TcCoercion
 606 -- Applied only to EvTerms of type (s~t)
 607 -- See Note [Coercion evidence terms]
 608 evTermCoercion (EvId v)        = mkTcCoVarCo v
 609 evTermCoercion (EvCoercion co) = co
 610 evTermCoercion (EvCast tm co)  = TcCastCo (evTermCoercion tm) co
 611 evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
 612
 613 evVarsOfTerm :: EvTerm -> VarSet
 614 evVarsOfTerm (EvId v)             = unitVarSet v
 615 evVarsOfTerm (EvCoercion co)      = coVarsOfTcCo co
 616 evVarsOfTerm (EvDFunApp _ _ evs)  = evVarsOfTerms evs
 617 evVarsOfTerm (EvTupleSel v _)     = evVarsOfTerm v
 618 evVarsOfTerm (EvSuperClass v _)   = evVarsOfTerm v
 619 evVarsOfTerm (EvCast tm co)       = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo co
 620 evVarsOfTerm (EvTupleMk evs)      = evVarsOfTerms evs
 621 evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
 622 evVarsOfTerm (EvKindCast v co)    = coVarsOfTcCo co `unionVarSet` evVarsOfTerm v
 623 evVarsOfTerm (EvLit _)            = emptyVarSet
 624
 625 evVarsOfTerms :: [EvTerm] -> VarSet
 626 evVarsOfTerms = foldr (unionVarSet . evVarsOfTerm) emptyVarSet
 627 \end{code}
 628
 629
 630 %************************************************************************
 631 %*                                                                      *
 632                   Pretty printing
 633 %*                                                                      *
 634 %************************************************************************
 635
 636 \begin{code}
 637 instance Outputable HsWrapper where
 638   ppr co_fn = pprHsWrapper (ptext (sLit "<>")) co_fn
 639
 640 pprHsWrapper :: SDoc -> HsWrapper -> SDoc
 641 -- In debug mode, print the wrapper
 642 -- otherwise just print what's inside
 643 pprHsWrapper doc wrap
 644   = getPprStyle (\ s -> if debugStyle s then (help (add_parens doc) wrap False) else doc)
 645   where
 646     help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
 647     -- True  <=> appears in function application position
 648     -- False <=> appears as body of let or lambda
 649     help it WpHole             = it
 650     help it (WpCompose f1 f2)  = help (help it f2) f1
 651     help it (WpCast co)   = add_parens $ sep [it False, nest 2 (ptext (sLit "|>")
 652                                               <+> pprParendTcCo co)]
 653     help it (WpEvApp id)  = no_parens  $ sep [it True, nest 2 (ppr id)]
 654     help it (WpTyApp ty)  = no_parens  $ sep [it True, ptext (sLit "@") <+> pprParendType ty]
 655     help it (WpEvLam id)  = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False]
 656     help it (WpTyLam tv)  = add_parens $ sep [ptext (sLit "/\\") <> pp_bndr tv, it False]
 657     help it (WpLet binds) = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False]
 658
 659     pp_bndr v = pprBndr LambdaBind v <> dot
 660
 661     add_parens, no_parens :: SDoc -> Bool -> SDoc
 662     add_parens d True  = parens d
 663     add_parens d False = d
 664     no_parens d _ = d
 665
 666 instance Outputable TcEvBinds where
 667   ppr (TcEvBinds v) = ppr v
 668   ppr (EvBinds bs)  = ptext (sLit "EvBinds") <> braces (vcat (map ppr (bagToList bs)))
 669
 670 instance Outputable EvBindsVar where
 671   ppr (EvBindsVar _ u) = ptext (sLit "EvBindsVar") <> angleBrackets (ppr u)
 672
 673 instance Outputable EvBind where
 674   ppr (EvBind v e)   = sep [ ppr v, nest 2 $ equals <+> ppr e ]
 675    -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
 676
 677 instance Outputable EvTerm where
 678   ppr (EvId v)           = ppr v
 679   ppr (EvCast v co)      = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co
 680   ppr (EvKindCast v co)  = ppr v <+> (ptext (sLit "`kind-cast`")) <+> pprParendTcCo co
 681   ppr (EvCoercion co)    = ptext (sLit "CO") <+> ppr co
 682   ppr (EvTupleSel v n)   = ptext (sLit "tupsel") <> parens (ppr (v,n))
 683   ppr (EvTupleMk vs)     = ptext (sLit "tupmk") <+> ppr vs
 684   ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))
 685   ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
 686   ppr (EvLit l)          = ppr l
 687   ppr (EvDelayedError ty msg) =     ptext (sLit "error")
 688                                 <+> sep [ char '@' <> ppr ty, ppr msg ]
 689
 690 instance Outputable EvLit where
 691   ppr (EvNum n) = integer n
 692   ppr (EvStr s) = text (show s)
 693 \end{code}
 694