TcEvidence.hs 36.3 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1
-- (c) The University of Glasgow 2006
2

3 4
{-# LANGUAGE CPP, DeriveDataTypeable #-}

5 6 7
module TcEvidence (

  -- HsWrapper
8
  HsWrapper(..),
9
  (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams,
10
  mkWpLams, mkWpLet, mkWpCastN, mkWpCastR, collectHsWrapBinders,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
11
  mkWpFun, mkWpFuns, idHsWrapper, isIdHsWrapper, pprHsWrapper,
12

13
  -- Evidence bindings
14
  TcEvBinds(..), EvBindsVar(..),
15
  EvBindMap(..), emptyEvBindMap, extendEvBinds,
16 17
  lookupEvBind, evBindMapBinds, foldEvBindMap, filterEvBindMap,
  isEmptyEvBindMap,
18
  EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
19
  evBindVar, isCoEvBindsVar,
20 21 22 23

  -- EvTerm (already a CoreExpr)
  EvTerm(..), EvExpr,
  evId, evCoercion, evCast, evDFunApp,  evSelector,
24
  mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, findNeededEvVars,
25

26
  evTermCoercion, evTermCoercion_maybe,
27
  EvCallStack(..),
28
  EvTypeable(..),
29 30

  -- TcCoercion
31 32
  TcCoercion, TcCoercionR, TcCoercionN, TcCoercionP, CoercionHole,
  Role(..), LeftOrRight(..), pickLR,
33
  mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo,
34
  mkTcTyConAppCo, mkTcAppCo, mkTcFunCo,
35
  mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
36
  mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSubCo,
37
  tcDowngradeRole,
Ningning Xie's avatar
Ningning Xie committed
38 39 40
  mkTcAxiomRuleCo, mkTcGReflRightCo, mkTcGReflLeftCo, mkTcPhantomCo,
  mkTcCoherenceLeftCo,
  mkTcCoherenceRightCo,
41 42 43
  mkTcKindCo,
  tcCoercionKind, coVarsOfTcCo,
  mkTcCoVarCo,
44
  isTcReflCo, isTcReflexiveCo,
45
  tcCoercionRole,
46
  unwrapIP, wrapIP
47 48 49
  ) where
#include "HsVersions.h"

50 51
import GhcPrelude

52
import Var
53
import CoAxiom
54
import Coercion
55 56
import PprCore ()   -- Instance OutputableBndr TyVar
import TcType
57
import Type
58
import TyCon
59
import Class( Class )
60
import PrelNames
61
import DynFlags   ( gopt, GeneralFlag(Opt_PrintTypecheckerElaboration) )
62 63 64
import VarEnv
import VarSet
import Name
65
import Pair
66

67 68 69 70 71
import CoreSyn
import Class ( classSCSelId )
import Id ( isEvVar )
import CoreFVs ( exprSomeFreeVars )

72 73
import Util
import Bag
74
import qualified Data.Data as Data
75
import Outputable
76
import SrcLoc
77
import Data.IORef( IORef )
David Feuer's avatar
David Feuer committed
78
import UniqSet
79

Austin Seipp's avatar
Austin Seipp committed
80
{-
81 82
Note [TcCoercions]
~~~~~~~~~~~~~~~~~~
83
| TcCoercions are a hack used by the typechecker. Normally,
84 85 86 87
Coercions have free variables of type (a ~# b): we call these
CoVars. However, the type checker passes around equality evidence
(boxed up) at type (a ~ b).

88 89 90 91
An TcCoercion is simply a Coercion whose free variables have may be either
boxed or unboxed. After we are done with typechecking the desugarer finds the
boxed free variables, unboxes them, and creates a resulting real Coercion with
kosher free variables.
92

Austin Seipp's avatar
Austin Seipp committed
93
-}
94

95
type TcCoercion  = Coercion
96 97
type TcCoercionN = CoercionN    -- A Nominal          coercion ~N
type TcCoercionR = CoercionR    -- A Representational coercion ~R
98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113
type TcCoercionP = CoercionP    -- a phantom coercion

mkTcReflCo             :: Role -> TcType -> TcCoercion
mkTcSymCo              :: TcCoercion -> TcCoercion
mkTcTransCo            :: TcCoercion -> TcCoercion -> TcCoercion
mkTcNomReflCo          :: TcType -> TcCoercionN
mkTcRepReflCo          :: TcType -> TcCoercionR
mkTcTyConAppCo         :: Role -> TyCon -> [TcCoercion] -> TcCoercion
mkTcAppCo              :: TcCoercion -> TcCoercionN -> TcCoercion
mkTcFunCo              :: Role -> TcCoercion -> TcCoercion -> TcCoercion
mkTcAxInstCo           :: Role -> CoAxiom br -> BranchIndex
                       -> [TcType] -> [TcCoercion] -> TcCoercion
mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType]
                       -> [TcCoercion] -> TcCoercionR
mkTcForAllCo           :: TyVar -> TcCoercionN -> TcCoercion -> TcCoercion
mkTcForAllCos          :: [(TyVar, TcCoercionN)] -> TcCoercion -> TcCoercion
114
mkTcNthCo              :: Role -> Int -> TcCoercion -> TcCoercion
115 116 117 118 119
mkTcLRCo               :: LeftOrRight -> TcCoercion -> TcCoercion
mkTcSubCo              :: TcCoercionN -> TcCoercionR
maybeTcSubCo           :: EqRel -> TcCoercion -> TcCoercion
tcDowngradeRole        :: Role -> Role -> TcCoercion -> TcCoercion
mkTcAxiomRuleCo        :: CoAxiomRule -> [TcCoercion] -> TcCoercionR
Ningning Xie's avatar
Ningning Xie committed
120 121 122 123 124 125
mkTcGReflRightCo       :: Role -> TcType -> TcCoercionN -> TcCoercion
mkTcGReflLeftCo        :: Role -> TcType -> TcCoercionN -> TcCoercion
mkTcCoherenceLeftCo    :: Role -> TcType -> TcCoercionN
                       -> TcCoercion -> TcCoercion
mkTcCoherenceRightCo   :: Role -> TcType -> TcCoercionN
                       -> TcCoercion -> TcCoercion
126 127 128 129 130 131 132 133 134
mkTcPhantomCo          :: TcCoercionN -> TcType -> TcType -> TcCoercionP
mkTcKindCo             :: TcCoercion -> TcCoercionN
mkTcCoVarCo            :: CoVar -> TcCoercion

tcCoercionKind         :: TcCoercion -> Pair TcType
tcCoercionRole         :: TcCoercion -> Role
coVarsOfTcCo           :: TcCoercion -> TcTyCoVarSet
isTcReflCo             :: TcCoercion -> Bool

135 136 137 138
-- | This version does a slow check, calculating the related types and seeing
-- if they are equal.
isTcReflexiveCo        :: TcCoercion -> Bool

139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156
mkTcReflCo             = mkReflCo
mkTcSymCo              = mkSymCo
mkTcTransCo            = mkTransCo
mkTcNomReflCo          = mkNomReflCo
mkTcRepReflCo          = mkRepReflCo
mkTcTyConAppCo         = mkTyConAppCo
mkTcAppCo              = mkAppCo
mkTcFunCo              = mkFunCo
mkTcAxInstCo           = mkAxInstCo
mkTcUnbranchedAxInstCo = mkUnbranchedAxInstCo Representational
mkTcForAllCo           = mkForAllCo
mkTcForAllCos          = mkForAllCos
mkTcNthCo              = mkNthCo
mkTcLRCo               = mkLRCo
mkTcSubCo              = mkSubCo
maybeTcSubCo           = maybeSubCo
tcDowngradeRole        = downgradeRole
mkTcAxiomRuleCo        = mkAxiomRuleCo
Ningning Xie's avatar
Ningning Xie committed
157 158
mkTcGReflRightCo       = mkGReflRightCo
mkTcGReflLeftCo        = mkGReflLeftCo
159 160 161 162 163 164 165 166 167 168
mkTcCoherenceLeftCo    = mkCoherenceLeftCo
mkTcCoherenceRightCo   = mkCoherenceRightCo
mkTcPhantomCo          = mkPhantomCo
mkTcKindCo             = mkKindCo
mkTcCoVarCo            = mkCoVarCo

tcCoercionKind         = coercionKind
tcCoercionRole         = coercionRole
coVarsOfTcCo           = coVarsOfCo
isTcReflCo             = isReflCo
169
isTcReflexiveCo        = isReflexiveCo
Joachim Breitner's avatar
Joachim Breitner committed
170

Austin Seipp's avatar
Austin Seipp committed
171
{-
172 173
%************************************************************************
%*                                                                      *
174
                  HsWrapper
Austin Seipp's avatar
Austin Seipp committed
175 176 177
*                                                                      *
************************************************************************
-}
178 179 180 181 182 183 184 185 186 187

data HsWrapper
  = WpHole                      -- The identity coercion

  | WpCompose HsWrapper HsWrapper
       -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
       --
       -- Hence  (\a. []) `WpCompose` (\b. []) = (\a b. [])
       -- But    ([] a)   `WpCompose` ([] b)   = ([] b a)

188
  | WpFun HsWrapper HsWrapper TcType SDoc
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
189
       -- (WpFun wrap1 wrap2 t1)[e] = \(x:t1). wrap2[ e wrap1[x] ]
190 191 192
       -- So note that if  wrap1 :: exp_arg <= act_arg
       --                  wrap2 :: act_res <= exp_res
       --           then   WpFun wrap1 wrap2 : (act_arg -> arg_res) <= (exp_arg -> exp_res)
193
       -- This isn't the same as for mkFunCo, but it has to be this way
194
       -- because we can't use 'sym' to flip around these HsWrappers
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
195
       -- The TcType is the "from" type of the first wrapper
196 197 198
       -- The SDoc explains the circumstances under which we have created this
       -- WpFun, in case we run afoul of levity polymorphism restrictions in
       -- the desugarer. See Note [Levity polymorphism checking] in DsMonad
199

200
  | WpCast TcCoercionR        -- A cast:  [] `cast` co
201
                              -- Guaranteed not the identity coercion
Joachim Breitner's avatar
Joachim Breitner committed
202
                              -- At role Representational
203 204 205

        -- Evidence abstraction and application
        -- (both dictionaries and coercions)
206 207
  | WpEvLam EvVar               -- \d. []       the 'd' is an evidence variable
  | WpEvApp EvTerm              -- [] d         the 'd' is evidence for a constraint
208 209 210 211 212 213 214 215
        -- Kind and Type abstraction and application
  | WpTyLam TyVar       -- \a. []  the 'a' is a type/kind variable (not coercion var)
  | WpTyApp KindOrType  -- [] t    the 't' is a type (not coercion)


  | WpLet TcEvBinds             -- Non-empty (or possibly non-empty) evidence bindings,
                                -- so that the identity coercion is always exactly WpHole

216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275
-- Cannot derive Data instance because SDoc is not Data (it stores a function).
-- So we do it manually:
instance Data.Data HsWrapper where
  gfoldl _ z WpHole             = z WpHole
  gfoldl k z (WpCompose a1 a2)  = z WpCompose `k` a1 `k` a2
  gfoldl k z (WpFun a1 a2 a3 _) = z wpFunEmpty `k` a1 `k` a2 `k` a3
  gfoldl k z (WpCast a1)        = z WpCast `k` a1
  gfoldl k z (WpEvLam a1)       = z WpEvLam `k` a1
  gfoldl k z (WpEvApp a1)       = z WpEvApp `k` a1
  gfoldl k z (WpTyLam a1)       = z WpTyLam `k` a1
  gfoldl k z (WpTyApp a1)       = z WpTyApp `k` a1
  gfoldl k z (WpLet a1)         = z WpLet `k` a1

  gunfold k z c = case Data.constrIndex c of
                    1 -> z WpHole
                    2 -> k (k (z WpCompose))
                    3 -> k (k (k (z wpFunEmpty)))
                    4 -> k (z WpCast)
                    5 -> k (z WpEvLam)
                    6 -> k (z WpEvApp)
                    7 -> k (z WpTyLam)
                    8 -> k (z WpTyApp)
                    _ -> k (z WpLet)

  toConstr WpHole          = wpHole_constr
  toConstr (WpCompose _ _) = wpCompose_constr
  toConstr (WpFun _ _ _ _) = wpFun_constr
  toConstr (WpCast _)      = wpCast_constr
  toConstr (WpEvLam _)     = wpEvLam_constr
  toConstr (WpEvApp _)     = wpEvApp_constr
  toConstr (WpTyLam _)     = wpTyLam_constr
  toConstr (WpTyApp _)     = wpTyApp_constr
  toConstr (WpLet _)       = wpLet_constr

  dataTypeOf _ = hsWrapper_dataType

hsWrapper_dataType :: Data.DataType
hsWrapper_dataType
  = Data.mkDataType "HsWrapper"
      [ wpHole_constr, wpCompose_constr, wpFun_constr, wpCast_constr
      , wpEvLam_constr, wpEvApp_constr, wpTyLam_constr, wpTyApp_constr
      , wpLet_constr]

wpHole_constr, wpCompose_constr, wpFun_constr, wpCast_constr, wpEvLam_constr,
  wpEvApp_constr, wpTyLam_constr, wpTyApp_constr, wpLet_constr :: Data.Constr
wpHole_constr    = mkHsWrapperConstr "WpHole"
wpCompose_constr = mkHsWrapperConstr "WpCompose"
wpFun_constr     = mkHsWrapperConstr "WpFun"
wpCast_constr    = mkHsWrapperConstr "WpCast"
wpEvLam_constr   = mkHsWrapperConstr "WpEvLam"
wpEvApp_constr   = mkHsWrapperConstr "WpEvApp"
wpTyLam_constr   = mkHsWrapperConstr "WpTyLam"
wpTyApp_constr   = mkHsWrapperConstr "WpTyApp"
wpLet_constr     = mkHsWrapperConstr "WpLet"

mkHsWrapperConstr :: String -> Data.Constr
mkHsWrapperConstr name = Data.mkConstr hsWrapper_dataType name [] Data.Prefix

wpFunEmpty :: HsWrapper -> HsWrapper -> TcType -> HsWrapper
wpFunEmpty c1 c2 t1 = WpFun c1 c2 t1 empty
276 277 278 279 280 281

(<.>) :: HsWrapper -> HsWrapper -> HsWrapper
WpHole <.> c = c
c <.> WpHole = c
c1 <.> c2    = c1 `WpCompose` c2

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
282 283 284 285
mkWpFun :: HsWrapper -> HsWrapper
        -> TcType    -- the "from" type of the first wrapper
        -> TcType    -- either type of the second wrapper (used only when the
                     -- second wrapper is the identity)
286
        -> SDoc      -- what caused you to want a WpFun? Something like "When converting ..."
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
287
        -> HsWrapper
288 289 290 291 292
mkWpFun WpHole       WpHole       _  _  _ = WpHole
mkWpFun WpHole       (WpCast co2) t1 _  _ = WpCast (mkTcFunCo Representational (mkTcRepReflCo t1) co2)
mkWpFun (WpCast co1) WpHole       _  t2 _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) (mkTcRepReflCo t2))
mkWpFun (WpCast co1) (WpCast co2) _  _  _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) co2)
mkWpFun co1          co2          t1 _  d = WpFun co1 co2 t1 d
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
293

294 295 296 297 298 299
-- | @mkWpFuns [(ty1, wrap1), (ty2, wrap2)] ty_res wrap_res@,
-- where @wrap1 :: ty1 "->" ty1'@ and @wrap2 :: ty2 "->" ty2'@,
-- @wrap3 :: ty3 "->" ty3'@ and @ty_res@ is /either/ @ty3@ or @ty3'@,
-- gives a wrapper @(ty1' -> ty2' -> ty3) "->" (ty1 -> ty2 -> ty3')@.
-- Notice that the result wrapper goes the other way round to all
-- the others. This is a result of sub-typing contravariance.
300 301 302
-- The SDoc is a description of what you were doing when you called mkWpFuns.
mkWpFuns :: [(TcType, HsWrapper)] -> TcType -> HsWrapper -> SDoc -> HsWrapper
mkWpFuns args res_ty res_wrap doc = snd $ go args res_ty res_wrap
303 304 305 306
  where
    go [] res_ty res_wrap = (res_ty, res_wrap)
    go ((arg_ty, arg_wrap) : args) res_ty res_wrap
      = let (tail_ty, tail_wrap) = go args res_ty res_wrap in
307
        (arg_ty `mkFunTy` tail_ty, mkWpFun arg_wrap tail_wrap arg_ty tail_ty doc)
308

309 310
mkWpCastR :: TcCoercionR -> HsWrapper
mkWpCastR co
311 312 313
  | isTcReflCo co = WpHole
  | otherwise     = ASSERT2(tcCoercionRole co == Representational, ppr co)
                    WpCast co
Joachim Breitner's avatar
Joachim Breitner committed
314

315 316 317 318 319 320 321
mkWpCastN :: TcCoercionN -> HsWrapper
mkWpCastN co
  | isTcReflCo co = WpHole
  | otherwise     = ASSERT2(tcCoercionRole co == Nominal, ppr co)
                    WpCast (mkTcSubCo co)
    -- The mkTcSubCo converts Nominal to Representational

322 323 324
mkWpTyApps :: [Type] -> HsWrapper
mkWpTyApps tys = mk_co_app_fn WpTyApp tys

325 326
mkWpEvApps :: [EvTerm] -> HsWrapper
mkWpEvApps args = mk_co_app_fn WpEvApp args
327 328

mkWpEvVarApps :: [EvVar] -> HsWrapper
329
mkWpEvVarApps vs = mk_co_app_fn WpEvApp (map (EvExpr . evId) vs)
330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356

mkWpTyLams :: [TyVar] -> HsWrapper
mkWpTyLams ids = mk_co_lam_fn WpTyLam ids

mkWpLams :: [Var] -> HsWrapper
mkWpLams ids = mk_co_lam_fn WpEvLam ids

mkWpLet :: TcEvBinds -> HsWrapper
-- This no-op is a quite a common case
mkWpLet (EvBinds b) | isEmptyBag b = WpHole
mkWpLet ev_binds                   = WpLet ev_binds

mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as

mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
-- For applications, the *first* argument must
-- come *last* in the composition sequence
mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as

idHsWrapper :: HsWrapper
idHsWrapper = WpHole

isIdHsWrapper :: HsWrapper -> Bool
isIdHsWrapper WpHole = True
isIdHsWrapper _      = False

357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373
collectHsWrapBinders :: HsWrapper -> ([Var], HsWrapper)
-- Collect the outer lambda binders of a HsWrapper,
-- stopping as soon as you get to a non-lambda binder
collectHsWrapBinders wrap = go wrap []
  where
    -- go w ws = collectHsWrapBinders (w <.> w1 <.> ... <.> wn)
    go :: HsWrapper -> [HsWrapper] -> ([Var], HsWrapper)
    go (WpEvLam v)       wraps = add_lam v (gos wraps)
    go (WpTyLam v)       wraps = add_lam v (gos wraps)
    go (WpCompose w1 w2) wraps = go w1 (w2:wraps)
    go wrap              wraps = ([], foldl (<.>) wrap wraps)

    gos []     = ([], WpHole)
    gos (w:ws) = go w ws

    add_lam v (vs,w) = (v:vs, w)

Austin Seipp's avatar
Austin Seipp committed
374 375 376
{-
************************************************************************
*                                                                      *
377
                  Evidence bindings
Austin Seipp's avatar
Austin Seipp committed
378 379 380
*                                                                      *
************************************************************************
-}
381 382 383 384 385 386 387 388 389

data TcEvBinds
  = TcEvBinds           -- Mutable evidence bindings
       EvBindsVar       -- Mutable because they are updated "later"
                        --    when an implication constraint is solved

  | EvBinds             -- Immutable after zonking
       (Bag EvBind)

390 391 392 393 394 395 396 397
data EvBindsVar
  = EvBindsVar {
      ebv_uniq :: Unique,
         -- The Unique is for debug printing only

      ebv_binds :: IORef EvBindMap,
      -- The main payload: the value-level evidence bindings
      --     (dictionaries etc)
398
      -- Some Given, some Wanted
399

400 401
      ebv_tcvs :: IORef CoVarSet
      -- The free coercion vars of the (rhss of) the coercion bindings
402
      -- All of these are Wanted
403 404 405 406 407 408 409
      --
      -- Coercions don't actually have bindings
      -- because we plug them in-place (via a mutable
      -- variable); but we keep their free variables
      -- so that we can report unused given constraints
      -- See Note [Tracking redundant constraints] in TcSimplify
    }
410

411
  | CoEvBindsVar {  -- See Note [Coercion evidence only]
412

413
      -- See above for comments on ebv_uniq, evb_tcvs
414 415 416 417
      ebv_uniq :: Unique,
      ebv_tcvs :: IORef CoVarSet
    }

418 419 420 421 422 423
instance Data.Data TcEvBinds where
  -- Placeholder; we can't travers into TcEvBinds
  toConstr _   = abstractConstr "TcEvBinds"
  gunfold _ _  = error "gunfold"
  dataTypeOf _ = Data.mkNoRepType "TcEvBinds"

424 425
{- Note [Coercion evidence only]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
426 427
Class constraints etc give rise to /term/ bindings for evidence, and
we have nowhere to put term bindings in /types/.  So in some places we
428
use CoEvBindsVar (see newCoTcEvBinds) to signal that no term-level
429 430 431 432 433 434 435 436 437
evidence bindings are allowed.  Notebly ():

  - Places in types where we are solving kind constraints (all of which
    are equalities); see solveEqualities, solveLocalEqualities,
    checkTvConstraints

  - When unifying forall-types
-}

438 439 440
isCoEvBindsVar :: EvBindsVar -> Bool
isCoEvBindsVar (CoEvBindsVar {}) = True
isCoEvBindsVar (EvBindsVar {})   = False
441

442
-----------------
443 444
newtype EvBindMap
  = EvBindMap {
445
       ev_bind_varenv :: DVarEnv EvBind
446
    }       -- Map from evidence variables to evidence terms
447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464
            -- We use @DVarEnv@ here to get deterministic ordering when we
            -- turn it into a Bag.
            -- If we don't do that, when we generate let bindings for
            -- dictionaries in dsTcEvBinds they will be generated in random
            -- order.
            --
            -- For example:
            --
            -- let $dEq = GHC.Classes.$fEqInt in
            -- let $$dNum = GHC.Num.$fNumInt in ...
            --
            -- vs
            --
            -- let $dNum = GHC.Num.$fNumInt in
            -- let $dEq = GHC.Classes.$fEqInt in ...
            --
            -- See Note [Deterministic UniqFM] in UniqDFM for explanation why
            -- @UniqFM@ can lead to nondeterministic order.
465 466

emptyEvBindMap :: EvBindMap
467
emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyDVarEnv }
468

469 470
extendEvBinds :: EvBindMap -> EvBind -> EvBindMap
extendEvBinds bs ev_bind
471 472 473
  = EvBindMap { ev_bind_varenv = extendDVarEnv (ev_bind_varenv bs)
                                               (eb_lhs ev_bind)
                                               ev_bind }
474

475 476 477
isEmptyEvBindMap :: EvBindMap -> Bool
isEmptyEvBindMap (EvBindMap m) = isEmptyDVarEnv m

478
lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
479
lookupEvBind bs = lookupDVarEnv (ev_bind_varenv bs)
480 481

evBindMapBinds :: EvBindMap -> Bag EvBind
482 483 484
evBindMapBinds = foldEvBindMap consBag emptyBag

foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
485
foldEvBindMap k z bs = foldDVarEnv k z (ev_bind_varenv bs)
486

487 488 489 490
filterEvBindMap :: (EvBind -> Bool) -> EvBindMap -> EvBindMap
filterEvBindMap k (EvBindMap { ev_bind_varenv = env })
  = EvBindMap { ev_bind_varenv = filterDVarEnv k env }

491 492 493
instance Outputable EvBindMap where
  ppr (EvBindMap m) = ppr m

494 495
-----------------
-- All evidence is bound by EvBinds; no side effects
496 497 498 499 500 501 502
data EvBind
  = EvBind { eb_lhs      :: EvVar
           , eb_rhs      :: EvTerm
           , eb_is_given :: Bool  -- True <=> given
                 -- See Note [Tracking redundant constraints] in TcSimplify
    }

503 504 505
evBindVar :: EvBind -> EvVar
evBindVar = eb_lhs

506 507 508
mkWantedEvBind :: EvVar -> EvTerm -> EvBind
mkWantedEvBind ev tm = EvBind { eb_is_given = False, eb_lhs = ev, eb_rhs = tm }

509
-- EvTypeable are never given, so we can work with EvExpr here instead of EvTerm
510 511
mkGivenEvBind :: EvVar -> EvTerm -> EvBind
mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = tm }
512

513

514 515 516 517
-- An EvTerm is, conceptually, a CoreExpr that implements the constraint.
-- Unfortunately, we cannot just do
--   type EvTerm  = CoreExpr
-- Because of staging problems issues around EvTypeable
518
data EvTerm
519 520 521 522 523 524 525 526 527 528 529
  = EvExpr EvExpr

  | EvTypeable Type EvTypeable   -- Dictionary for (Typeable ty)

  | EvFun     -- /\as \ds. let binds in v
      { et_tvs   :: [TyVar]
      , et_given :: [EvVar]
      , et_binds :: TcEvBinds -- This field is why we need an EvFun
                              -- constructor, and can't just use EvExpr
      , et_body  :: EvVar }

530
  deriving Data.Data
531

532
type EvExpr = CoreExpr
533

534 535
-- An EvTerm is (usually) constructed by any of the constructors here
-- and those more complicates ones who were moved to module TcEvTerm
536

537 538 539
-- | Any sort of evidence Id, including coercions
evId ::  EvId -> EvExpr
evId = Var
540

541 542
-- coercion bindings
-- See Note [Coercion evidence terms]
543 544
evCoercion :: TcCoercion -> EvTerm
evCoercion co = EvExpr (Coercion co)
545

546
-- | d |> co
547 548 549
evCast :: EvExpr -> TcCoercion -> EvTerm
evCast et tc | isReflCo tc = EvExpr et
             | otherwise   = EvExpr (Cast et tc)
550

551
-- Dictionary instance application
552 553
evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvTerm
evDFunApp df tys ets = EvExpr $ Var df `mkTyApps` tys `mkApps` ets
554

555 556 557 558 559 560
-- Selector id plus the types at which it
-- should be instantiated, used for HasField
-- dictionaries; see Note [HasField instances]
-- in TcInterface
evSelector :: Id -> [Type] -> [EvExpr] -> EvExpr
evSelector sel_id tys tms = Var sel_id `mkTyApps` tys `mkApps` tms
561

562 563 564
-- Dictionary for (Typeable ty)
evTypeable :: Type -> EvTypeable -> EvTerm
evTypeable = EvTypeable
565

566
-- | Instructions on how to make a 'Typeable' dictionary.
567
-- See Note [Typeable evidence terms]
568
data EvTypeable
Ben Gamari's avatar
Ben Gamari committed
569 570 571 572
  = EvTypeableTyCon TyCon [EvTerm]
    -- ^ Dictionary for @Typeable T@ where @T@ is a type constructor with all of
    -- its kind variables saturated. The @[EvTerm]@ is @Typeable@ evidence for
    -- the applied kinds..
573

574 575
  | EvTypeableTyApp EvTerm EvTerm
    -- ^ Dictionary for @Typeable (s t)@,
Ben Gamari's avatar
Ben Gamari committed
576 577 578 579 580
    -- given a dictionaries for @s@ and @t@.

  | EvTypeableTrFun EvTerm EvTerm
    -- ^ Dictionary for @Typeable (s -> t)@,
    -- given a dictionaries for @s@ and @t@.
581

582 583 584 585 586
  | EvTypeableTyLit EvTerm
    -- ^ Dictionary for a type literal,
    -- e.g. @Typeable "foo"@ or @Typeable 3@
    -- The 'EvTerm' is evidence of, e.g., @KnownNat 3@
    -- (see Trac #10348)
587
  deriving Data.Data
588

589 590 591 592
-- | Evidence for @CallStack@ implicit parameters.
data EvCallStack
  -- See Note [Overview of implicit CallStacks]
  = EvCsEmpty
593
  | EvCsPushCall Name RealSrcSpan EvExpr
594 595
    -- ^ @EvCsPushCall name loc stk@ represents a call to @name@, occurring at
    -- @loc@, in a calling context @stk@.
596
  deriving Data.Data
597

Austin Seipp's avatar
Austin Seipp committed
598
{-
599 600 601 602 603 604 605 606 607
Note [Typeable evidence terms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The EvTypeable data type looks isomorphic to Type, but the EvTerms
inside can be EvIds.  Eg
    f :: forall a. Typeable a => a -> TypeRep
    f x = typeRep (undefined :: Proxy [a])
Here for the (Typeable [a]) dictionary passed to typeRep we make
evidence
    dl :: Typeable [a] = EvTypeable [a]
608
                            (EvTypeableTyApp (EvTypeableTyCon []) (EvId d))
609 610 611 612
where
    d :: Typable a
is the lambda-bound dictionary passed into f.

613 614
Note [Coercion evidence terms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
615
A "coercion evidence term" takes one of these forms
616
   co_tm ::= EvId v           where v :: t1 ~# t2
617 618
           | EvCoercion co
           | EvCast co_tm co
Simon Peyton Jones's avatar
Simon Peyton Jones committed
619 620

We do quite often need to get a TcCoercion from an EvTerm; see
621
'evTermCoercion'.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
622

623
INVARIANT: The evidence for any constraint with type (t1 ~# t2) is
624
a coercion evidence term.  Consider for example
625
    [G] d :: F Int a
626 627 628
If we have
    ax7 a :: F Int a ~ (a ~ Bool)
then we do NOT generate the constraint
629
    [G] (d |> ax7 a) :: a ~ Bool
630
because that does not satisfy the invariant (d is not a coercion variable).
631
Instead we make a binding
632 633 634
    g1 :: a~Bool = g |> ax7 a
and the constraint
    [G] g1 :: a~Bool
635
See Trac [7238] and Note [Bind new Givens immediately] in TcRnTypes
Simon Peyton Jones's avatar
Simon Peyton Jones committed
636

637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654
Note [EvBinds/EvTerm]
~~~~~~~~~~~~~~~~~~~~~
How evidence is created and updated. Bindings for dictionaries,
and coercions and implicit parameters are carried around in TcEvBinds
which during constraint generation and simplification is always of the
form (TcEvBinds ref). After constraint simplification is finished it
will be transformed to t an (EvBinds ev_bag).

Evidence for coercions *SHOULD* be filled in using the TcEvBinds
However, all EvVars that correspond to *wanted* coercion terms in
an EvBind must be mutable variables so that they can be readily
inlined (by zonking) after constraint simplification is finished.

Conclusion: a new wanted coercion variable should be made mutable.
[Notice though that evidence variables that bind coercion terms
 from super classes will be "given" and hence rigid]


655 656 657 658 659 660 661
Note [Overview of implicit CallStacks]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(See https://ghc.haskell.org/trac/ghc/wiki/ExplicitCallStack/ImplicitLocations)

The goal of CallStack evidence terms is to reify locations
in the program source as runtime values, without any support
from the RTS. We accomplish this by assigning a special meaning
662
to constraints of type GHC.Stack.Types.HasCallStack, an alias
663

664 665 666 667
  type HasCallStack = (?callStack :: CallStack)

Implicit parameters of type GHC.Stack.Types.CallStack (the name is not
important) are solved in three steps:
668

669 670
1. Occurrences of CallStack IPs are solved directly from the given IP,
   just like a regular IP. For example, the occurrence of `?stk` in
671

672
     error :: (?stk :: CallStack) => String -> a
673
     error s = raise (ErrorCall (s ++ prettyCallStack ?stk))
674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691

   will be solved for the `?stk` in `error`s context as before.

2. In a function call, instead of simply passing the given IP, we first
   append the current call-site to it. For example, consider a
   call to the callstack-aware `error` above.

     undefined :: (?stk :: CallStack) => a
     undefined = error "undefined!"

   Here we want to take the given `?stk` and append the current
   call-site, before passing it to `error`. In essence, we want to
   rewrite `error "undefined!"` to

     let ?stk = pushCallStack <error's location> ?stk
     in error "undefined!"

   We achieve this effect by emitting a NEW wanted
692

693
     [W] d :: IP "stk" CallStack
694

695
   from which we build the evidence term
696

697
     EvCsPushCall "error" <error's location> (EvId d)
698

699 700
   that we use to solve the call to `error`. The new wanted `d` will
   then be solved per rule (1), ie as a regular IP.
701

702
   (see TcInteract.interactDict)
703

704 705
3. We default any insoluble CallStacks to the empty CallStack. Suppose
   `undefined` did not request a CallStack, ie
706

707 708
     undefinedNoStk :: a
     undefinedNoStk = error "undefined!"
709

710 711 712
   Under the usual IP rules, the new wanted from rule (2) would be
   insoluble as there's no given IP from which to solve it, so we
   would get an "unbound implicit parameter" error.
713

714 715 716
   We don't ever want to emit an insoluble CallStack IP, so we add a
   defaulting pass to default any remaining wanted CallStacks to the
   empty CallStack with the evidence term
717

718
     EvCsEmpty
719

720
   (see TcSimplify.simpl_top and TcSimplify.defaultCallStacks)
721 722 723 724

This provides a lightweight mechanism for building up call-stacks
explicitly, but is notably limited by the fact that the stack will
stop at the first function whose type does not include a CallStack IP.
725
For example, using the above definition of `undefined`:
726

727 728 729 730 731
  head :: [a] -> a
  head []    = undefined
  head (x:_) = x

  g = head []
732

733 734 735
the resulting CallStack will include the call to `undefined` in `head`
and the call to `error` in `undefined`, but *not* the call to `head`
in `g`, because `head` did not explicitly request a CallStack.
736 737 738 739 740


Important Details:
- GHC should NEVER report an insoluble CallStack constraint.

Eric Seidel's avatar
Eric Seidel committed
741 742 743
- GHC should NEVER infer a CallStack constraint unless one was requested
  with a partial type signature (See TcType.pickQuantifiablePreds).

744 745 746 747 748 749
- A CallStack (defined in GHC.Stack.Types) is a [(String, SrcLoc)],
  where the String is the name of the binder that is used at the
  SrcLoc. SrcLoc is also defined in GHC.Stack.Types and contains the
  package/module/file name, as well as the full source-span. Both
  CallStack and SrcLoc are kept abstract so only GHC can construct new
  values.
750

751 752
- We will automatically solve any wanted CallStack regardless of the
  name of the IP, i.e.
753 754 755 756 757 758 759 760 761 762 763

    f = show (?stk :: CallStack)
    g = show (?loc :: CallStack)

  are both valid. However, we will only push new SrcLocs onto existing
  CallStacks when the IP names match, e.g. in

    head :: (?loc :: CallStack) => [a] -> a
    head [] = error (show (?stk :: CallStack))

  the printed CallStack will NOT include head's call-site. This reflects the
764
  standard scoping rules of implicit-parameters.
765 766 767 768 769

- An EvCallStack term desugars to a CoreExpr of type `IP "some str" CallStack`.
  The desugarer will need to unwrap the IP newtype before pushing a new
  call-site onto a given stack (See DsBinds.dsEvCallStack)

770 771 772
- When we emit a new wanted CallStack from rule (2) we set its origin to
  `IPOccOrigin ip_name` instead of the original `OccurrenceOf func`
  (see TcInteract.interactDict).
773

774 775
  This is a bit shady, but is how we ensure that the new wanted is
  solved like a regular IP.
776

Austin Seipp's avatar
Austin Seipp committed
777
-}
778

779
mkEvCast :: EvExpr -> TcCoercion -> EvTerm
780
mkEvCast ev lco
781 782 783
  | ASSERT2( tcCoercionRole lco == Representational
           , (vcat [text "Coercion of wrong role passed to mkEvCast:", ppr ev, ppr lco]))
    isTcReflCo lco = EvExpr ev
784
  | otherwise      = evCast ev lco
785

786 787 788 789 790 791 792

mkEvScSelectors         -- Assume   class (..., D ty, ...) => C a b
  :: Class -> [TcType]  -- C ty1 ty2
  -> [(TcPredType,      -- D ty[ty1/a,ty2/b]
       EvExpr)          -- :: C ty1 ty2 -> D ty[ty1/a,ty2/b]
     ]
mkEvScSelectors cls tys
793 794
   = zipWith mk_pr (immSuperClasses cls tys) [0..]
  where
795
    mk_pr pred i = (pred, Var sc_sel_id `mkTyApps` tys)
796 797
      where
        sc_sel_id  = classSCSelId cls i -- Zero-indexed
798

799 800 801 802 803 804 805
emptyTcEvBinds :: TcEvBinds
emptyTcEvBinds = EvBinds emptyBag

isEmptyTcEvBinds :: TcEvBinds -> Bool
isEmptyTcEvBinds (EvBinds b)    = isEmptyBag b
isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"

806
evTermCoercion_maybe :: EvTerm -> Maybe TcCoercion
807
-- Applied only to EvTerms of type (s~t)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
808
-- See Note [Coercion evidence terms]
809 810 811 812 813 814 815 816 817 818
evTermCoercion_maybe ev_term
  | EvExpr e <- ev_term = go e
  | otherwise           = Nothing
  where
    go :: EvExpr -> Maybe TcCoercion
    go (Var v)       = return (mkCoVarCo v)
    go (Coercion co) = return co
    go (Cast tm co)  = do { co' <- go tm
                          ; return (mkCoCast co' co) }
    go _             = Nothing
819

820 821 822 823 824 825 826
evTermCoercion :: EvTerm -> TcCoercion
evTermCoercion tm = case evTermCoercion_maybe tm of
                      Just co -> co
                      Nothing -> pprPanic "evTermCoercion" (ppr tm)


{- *********************************************************************
827 828 829
*                                                                      *
                  Free variables
*                                                                      *
830
********************************************************************* -}
831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849

findNeededEvVars :: EvBindMap -> VarSet -> VarSet
findNeededEvVars ev_binds seeds
  = transCloVarSet also_needs seeds
  where
   also_needs :: VarSet -> VarSet
   also_needs needs = nonDetFoldUniqSet add emptyVarSet needs
     -- It's OK to use nonDetFoldUFM here because we immediately
     -- forget about the ordering by creating a set

   add :: Var -> VarSet -> VarSet
   add v needs
     | Just ev_bind <- lookupEvBind ev_binds v
     , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
     , is_given
     = evVarsOfTerm rhs `unionVarSet` needs
     | otherwise
     = needs

850
evVarsOfTerm :: EvTerm -> VarSet
851 852
evVarsOfTerm (EvExpr e)         = exprSomeFreeVars isEvVar e
evVarsOfTerm (EvTypeable _ ev)  = evVarsOfTypeable ev
853
evVarsOfTerm (EvFun {})         = emptyVarSet -- See Note [Free vars of EvFun]
854 855

evVarsOfTerms :: [EvTerm] -> VarSet
856
evVarsOfTerms = mapUnionVarSet evVarsOfTerm
857

858 859 860 861 862 863 864 865
evVarsOfTypeable :: EvTypeable -> VarSet
evVarsOfTypeable ev =
  case ev of
    EvTypeableTyCon _ e   -> mapUnionVarSet evVarsOfTerm e
    EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2]
    EvTypeableTrFun e1 e2 -> evVarsOfTerms [e1,e2]
    EvTypeableTyLit e     -> evVarsOfTerm e

866

867 868 869 870 871 872 873 874 875 876 877 878
{- Note [Free vars of EvFun]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Finding the free vars of an EvFun is made tricky by the fact the
bindings et_binds may be a mutable variable.  Fortunately, we
can just squeeze by.  Here's how.

* evVarsOfTerm is used only by TcSimplify.neededEvVars.
* Each EvBindsVar in an et_binds field of an EvFun is /also/ in the
  ic_binds field of an Implication
* So we can track usage via the processing for that implication,
  (see Note [Tracking redundant constraints] in TcSimplify).
  We can ignore usage from the EvFun altogether.
879

Austin Seipp's avatar
Austin Seipp committed
880 881
************************************************************************
*                                                                      *
882
                  Pretty printing
Austin Seipp's avatar
Austin Seipp committed
883 884 885
*                                                                      *
************************************************************************
-}
886 887

instance Outputable HsWrapper where
888 889
  ppr co_fn = pprHsWrapper co_fn (no_parens (text "<>"))

890
pprHsWrapper :: HsWrapper -> (Bool -> SDoc) -> SDoc
891 892 893 894 895
-- With -fprint-typechecker-elaboration, print the wrapper
--   otherwise just print what's inside
-- The pp_thing_inside function takes Bool to say whether
--    it's in a position that needs parens for a non-atomic thing
pprHsWrapper wrap pp_thing_inside
896
  = sdocWithDynFlags $ \ dflags ->
897 898 899
    if gopt Opt_PrintTypecheckerElaboration dflags
    then help pp_thing_inside wrap False
    else pp_thing_inside False
900 901 902 903 904 905
  where
    help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
    -- True  <=> appears in function application position
    -- False <=> appears as body of let or lambda
    help it WpHole             = it
    help it (WpCompose f1 f2)  = help (help it f2) f1
906
    help it (WpFun f1 f2 t1 _) = add_parens $ text "\\(x" <> dcolon <> ppr t1 <> text ")." <+>
907 908
                                              help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False
    help it (WpCast co)   = add_parens $ sep [it False, nest 2 (text "|>"
909
                                              <+> pprParendCo co)]
910 911
    help it (WpEvApp id)  = no_parens  $ sep [it True, nest 2 (ppr id)]
    help it (WpTyApp ty)  = no_parens  $ sep [it True, text "@" <+> pprParendType ty]
912 913
    help it (WpEvLam id)  = add_parens $ sep [ text "\\" <> pprLamBndr id <> dot, it False]
    help it (WpTyLam tv)  = add_parens $ sep [text "/\\" <> pprLamBndr tv <> dot, it False]
914
    help it (WpLet binds) = add_parens $ sep [text "let" <+> braces (ppr binds), it False]
915

916 917
pprLamBndr :: Id -> SDoc
pprLamBndr v = pprBndr LambdaBind v
918

919 920 921 922
add_parens, no_parens :: SDoc -> Bool -> SDoc
add_parens d True  = parens d
add_parens d False = d
no_parens d _ = d
923 924 925

instance Outputable TcEvBinds where
  ppr (TcEvBinds v) = ppr v
926
  ppr (EvBinds bs)  = text "EvBinds" <> braces (vcat (map ppr (bagToList bs)))
927 928

instance Outputable EvBindsVar where
929 930
  ppr (EvBindsVar { ebv_uniq = u })
     = text "EvBindsVar" <> angleBrackets (ppr u)
931 932
  ppr (CoEvBindsVar { ebv_uniq = u })
     = text "CoEvBindsVar" <> angleBrackets (ppr u)
933

934
instance Uniquable EvBindsVar where
935
  getUnique = ebv_uniq
936

937
instance Outputable EvBind where
938 939 940 941
  ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given })
     = sep [ pp_gw <+> ppr v
           , nest 2 $ equals <+> ppr e ]
     where
942
       pp_gw = brackets (if is_given then char 'G' else char 'W')
943 944 945
   -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing

instance Outputable EvTerm where
946 947
  ppr (EvExpr e)         = ppr e
  ppr (EvTypeable ty ev) = ppr ev <+> dcolon <+> text "Typeable" <+> ppr ty
948 949 950
  ppr (EvFun { et_tvs = tvs, et_given = gs, et_binds = bs, et_body = w })
      = hang (text "\\" <+> sep (map pprLamBndr (tvs ++ gs)) <+> arrow)
           2 (ppr bs $$ ppr w)   -- Not very pretty
951 952 953

instance Outputable EvCallStack where
  ppr EvCsEmpty
954
    = text "[]"
955
  ppr (EvCsPushCall name loc tm)
956
    = ppr (name,loc) <+> text ":" <+> ppr tm
957

958
instance Outputable EvTypeable where
Ben Gamari's avatar
Ben Gamari committed
959
  ppr (EvTypeableTyCon ts _)  = text "TyCon" <+> ppr ts
960
  ppr (EvTypeableTyApp t1 t2) = parens (ppr t1 <+> ppr t2)
Ben Gamari's avatar
Ben Gamari committed
961
  ppr (EvTypeableTrFun t1 t2) = parens (ppr t1 <+> arrow <+> ppr t2)
962
  ppr (EvTypeableTyLit t1)    = text "TyLit" <> ppr t1
963 964


965 966 967 968
----------------------------------------------------------------------
-- Helper functions for dealing with IP newtype-dictionaries
----------------------------------------------------------------------

Adam Gundry's avatar
Adam Gundry committed
969 970 971 972 973 974
-- | Create a 'Coercion' that unwraps an implicit-parameter or
-- overloaded-label dictionary to expose the underlying value. We
-- expect the 'Type' to have the form `IP sym ty` or `IsLabel sym ty`,
-- and return a 'Coercion' `co :: IP sym ty ~ ty` or
-- `co :: IsLabel sym ty ~ Proxy# sym -> ty`.  See also
-- Note [Type-checking overloaded labels] in TcExpr.
975
unwrapIP :: Type -> CoercionR
976 977
unwrapIP ty =
  case unwrapNewTyCon_maybe tc of
978
    Just (_,_,ax) -> mkUnbranchedAxInstCo Representational ax tys []
979 980 981 982 983 984 985 986
    Nothing       -> pprPanic "unwrapIP" $
                       text "The dictionary for" <+> quotes (ppr tc)
                         <+> text "is not a newtype!"
  where
  (tc, tys) = splitTyConApp ty

-- | Create a 'Coercion' that wraps a value in an implicit-parameter
-- dictionary. See 'unwrapIP'.
987
wrapIP :: Type -> CoercionR
988
wrapIP ty = mkSymCo (unwrapIP ty)