Coercion.hs 110 KB
Newer Older
1 2 3
{-
(c) The University of Glasgow 2006
-}
4

5 6
{-# LANGUAGE RankNTypes, CPP, MultiWayIf, FlexibleContexts, BangPatterns,
             ScopedTypeVariables #-}
7

8
-- | Module for (a) type kinds and (b) type coercions,
9
-- as used in System FC. See 'CoreSyn.Expr' for
batterseapower's avatar
batterseapower committed
10 11
-- more on System FC and how coercions fit into it.
--
12
module Coercion (
batterseapower's avatar
batterseapower committed
13
        -- * Main data type
Ningning Xie's avatar
Ningning Xie committed
14
        Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionR,
15 16
        UnivCoProvenance, CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
        LeftOrRight(..),
17
        Var, CoVar, TyCoVar,
18
        Role(..), ltRole,
19

dreixel's avatar
dreixel committed
20
        -- ** Functions over coercions
21 22
        coVarTypes, coVarKind, coVarKindsTypesRole, coVarRole,
        coercionType, coercionKind, coercionKinds,
batterseapower's avatar
batterseapower committed
23
        mkCoercionType,
24
        coercionRole, coercionKindRole,
25

26
        -- ** Constructing coercions
Ningning Xie's avatar
Ningning Xie committed
27
        mkGReflCo, mkReflCo, mkRepReflCo, mkNomReflCo,
28 29 30 31
        mkCoVarCo, mkCoVarCos,
        mkAxInstCo, mkUnbranchedAxInstCo,
        mkAxInstRHS, mkUnbranchedAxInstRHS,
        mkAxInstLHS, mkUnbranchedAxInstLHS,
32
        mkPiCo, mkPiCos, mkCoCast,
33
        mkSymCo, mkTransCo, mkTransMCo,
34
        mkNthCo, nthCoRole, mkLRCo,
35
        mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo,
Ningning Xie's avatar
Ningning Xie committed
36
        mkForAllCo, mkForAllCos, mkHomoForAllCos,
37
        mkPhantomCo,
38
        mkUnsafeCo, mkHoleCo, mkUnivCo, mkSubCo,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
39
        mkAxiomInstCo, mkProofIrrelCo,
40
        downgradeRole, maybeSubCo, mkAxiomRuleCo,
Ningning Xie's avatar
Ningning Xie committed
41 42
        mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
        mkKindCo, castCoercionKind, castCoercionKindI,
43 44

        mkHeteroCoercionType,
TomSchrijvers's avatar
TomSchrijvers committed
45

46
        -- ** Decomposition
47
        instNewTyCon_maybe,
48 49

        NormaliseStepper, NormaliseStepResult(..), composeSteppers,
50 51
        mapStepResult, unwrapNewTypeStepper,
        topNormaliseNewType_maybe, topNormaliseTypeX,
52

53
        decomposeCo, decomposeFunCo, decomposePiCos, getCoVar_maybe,
54
        splitTyConAppCo_maybe,
55
        splitAppCo_maybe,
56
        splitFunCo_maybe,
57
        splitForAllCo_maybe,
Ningning Xie's avatar
Ningning Xie committed
58
        splitForAllCo_ty_maybe, splitForAllCo_co_maybe,
59

60
        nthRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
61 62 63

        pickLR,

Ningning Xie's avatar
Ningning Xie committed
64
        isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
65
        isReflCoVar_maybe,
66

67
        -- ** Coercion variables
68 69
        mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,
        isCoVar_maybe,
70 71

        -- ** Free variables
72
        tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo,
niteria's avatar
niteria committed
73
        tyCoFVsOfCo, tyCoFVsOfCos, tyCoVarsOfCoDSet,
74
        coercionSize,
75

76
        -- ** Substitution
77
        CvSubstEnv, emptyCvSubstEnv,
78 79 80
        lookupCoVar,
        substCo, substCos, substCoVar, substCoVars, substCoWith,
        substCoVarBndr,
81
        extendTvSubstAndInScope, getCvSubstEnv,
82

83
        -- ** Lifting
84
        liftCoSubst, liftCoSubstTyVar, liftCoSubstWith, liftCoSubstWithEx,
85
        emptyLiftingContext, extendLiftingContext, extendLiftingContextAndInScope,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
86
        liftCoSubstVarBndrUsing, isMappedByLC,
87 88

        mkSubstLiftingContext, zapLiftingContext,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
89
        substForAllCoBndrUsingLC, lcTCvSubst, lcInScopeSet,
90 91 92

        LiftCoEnv, LiftingContext(..), liftEnvSubstLeft, liftEnvSubstRight,
        substRightCo, substLeftCo, swapLiftCoEnv, lcSubstLeft, lcSubstRight,
93

batterseapower's avatar
batterseapower committed
94
        -- ** Comparison
95
        eqCoercion, eqCoercionX,
96

97 98
        -- ** Forcing evaluation of coercions
        seqCo,
99

100
        -- * Pretty-printing
101
        pprCo, pprParendCo,
102 103
        pprCoAxiom, pprCoAxBranch, pprCoAxBranchLHS,
        pprCoAxBranchUser, tidyCoAxBndrsForUser,
104
        etaExpandCoAxBranch,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
105 106 107

        -- * Tidying
        tidyCo, tidyCos,
TomSchrijvers's avatar
TomSchrijvers committed
108

109
        -- * Other
110 111 112
        promoteCoercion, buildCoercion,

        simplifyArgsWorker
113
       ) where
114 115 116

#include "HsVersions.h"

117 118
import {-# SOURCE #-} ToIface (toIfaceTyCon, tidyToIfaceTcArgs)

119 120
import GhcPrelude

121
import IfaceType
122 123
import TyCoRep
import Type
124
import TyCon
125
import CoAxiom
126
import Var
127
import VarEnv
128
import VarSet
129
import Name hiding ( varName )
130 131
import Util
import BasicTypes
132
import Outputable
133 134
import Unique
import Pair
Simon Peyton Jones's avatar
Simon Peyton Jones committed
135
import SrcLoc
136 137 138 139
import PrelNames
import TysPrim          ( eqPhantPrimTyCon )
import ListSetOps
import Maybes
140
import UniqFM
141

142
import Control.Monad (foldM, zipWithM)
143
import Data.Function ( on )
144
import Data.Char( isDigit )
145

146 147 148
{-
%************************************************************************
%*                                                                      *
149
     -- The coercion arguments always *precisely* saturate
150
     -- arity of (that branch of) the CoAxiom.  If there are
151
     -- any left over, we use AppCo.  See
Simon Peyton Jones's avatar
Simon Peyton Jones committed
152
     -- See [Coercion axioms applied to coercions] in TyCoRep
153

154
\subsection{Coercion variables}
155 156
%*                                                                      *
%************************************************************************
157
-}
158 159 160 161 162 163 164 165 166 167

coVarName :: CoVar -> Name
coVarName = varName

setCoVarUnique :: CoVar -> Unique -> CoVar
setCoVarUnique = setVarUnique

setCoVarName :: CoVar -> Name -> CoVar
setCoVarName   = setVarName

168
{-
169 170
%************************************************************************
%*                                                                      *
171
                   Pretty-printing CoAxioms
172 173
%*                                                                      *
%************************************************************************
174

175
Defined here to avoid module loops. CoAxiom is loaded very early on.
176

177
-}
178

179 180 181 182 183 184 185 186 187 188 189 190 191
etaExpandCoAxBranch :: CoAxBranch -> ([TyVar], [Type], Type)
-- Return the (tvs,lhs,rhs) after eta-expanding,
-- to the way in which the axiom was originally written
-- See Note [Eta reduction for data families] in CoAxiom
etaExpandCoAxBranch (CoAxBranch { cab_tvs = tvs
                                , cab_eta_tvs = eta_tvs
                                , cab_lhs = lhs
                                , cab_rhs = rhs })
  -- ToDo: what about eta_cvs?
  = (tvs ++ eta_tvs, lhs ++ eta_tys, mkAppTys rhs eta_tys)
 where
    eta_tys = mkTyVarTys eta_tvs

192
pprCoAxiom :: CoAxiom br -> SDoc
193 194
-- Used in debug-printing only
pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
195
  = hang (text "axiom" <+> ppr ax <+> dcolon)
196
       2 (vcat (map (pprCoAxBranchUser tc) (fromBranches branches)))
197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216

pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc
-- Used when printing injectivity errors (FamInst.makeInjectivityErrors)
-- and inaccessible branches (TcValidity.inaccessibleCoAxBranch)
-- This happens in error messages: don't print the RHS of a data
--   family axiom, which is meaningless to a user
pprCoAxBranchUser tc br
  | isDataFamilyTyCon tc = pprCoAxBranchLHS tc br
  | otherwise            = pprCoAxBranch    tc br

pprCoAxBranchLHS :: TyCon -> CoAxBranch -> SDoc
-- Print the family-instance equation when reporting
--   a conflict between equations (FamInst.conflictInstErr)
-- For type families the RHS is important; for data families not so.
--   Indeed for data families the RHS is a mysterious internal
--   type constructor, so we suppress it (Trac #14179)
-- See FamInstEnv Note [Family instance overlap conflicts]
pprCoAxBranchLHS = ppr_co_ax_branch pp_rhs
  where
    pp_rhs _ _ = empty
217

218 219
pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
pprCoAxBranch = ppr_co_ax_branch ppr_rhs
220
  where
221 222 223 224 225
    ppr_rhs env rhs = equals <+> pprPrecTypeX env topPrec rhs

ppr_co_ax_branch :: (TidyEnv -> Type -> SDoc)
                 -> TyCon -> CoAxBranch -> SDoc
ppr_co_ax_branch ppr_rhs fam_tc branch
226
  = foldr1 (flip hangNotEmpty 2)
227 228 229 230
    [ pprUserForAll (mkTyCoVarBinders Inferred bndrs')
         -- See Note [Printing foralls in type family instances] in IfaceType
    , pp_lhs <+> ppr_rhs tidy_env ee_rhs
    , text "-- Defined" <+> pp_loc ]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
231
  where
232 233 234 235 236 237 238 239 240 241 242 243
    loc = coAxBranchSpan branch
    pp_loc | isGoodSrcSpan loc = text "at" <+> ppr (srcSpanStart loc)
           | otherwise         = text "in" <+> ppr loc

    -- Eta-expand LHS and RHS types, because sometimes data family
    -- instances are eta-reduced.
    -- See Note [Eta reduction for data families] in FamInstEnv.
    (ee_tvs, ee_lhs, ee_rhs) = etaExpandCoAxBranch branch

    pp_lhs = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc)
                             (tidyToIfaceTcArgs tidy_env fam_tc ee_lhs)

244
    (tidy_env, bndrs') = tidyCoAxBndrsForUser emptyTidyEnv ee_tvs
245

246
tidyCoAxBndrsForUser :: TidyEnv -> [Var] -> (TidyEnv, [Var])
247 248 249 250 251 252 253 254
-- Tidy wildcards "_1", "_2" to "_", and do not return them
-- in the list of binders to be printed
-- This is so that in error messages we see
--     forall a. F _ [a] _ = ...
-- rather than
--     forall a _1 _2. F _1 [a] _2 = ...
--
-- This is a rather disgusting function
255
tidyCoAxBndrsForUser init_env tcvs
256 257
  = (tidy_env, reverse tidy_bndrs)
  where
258
    (tidy_env, tidy_bndrs) = foldl tidy_one (init_env, []) tcvs
259 260 261 262 263 264 265 266 267 268 269 270 271 272 273

    tidy_one (env@(occ_env, subst), rev_bndrs') bndr
      | is_wildcard bndr = (env_wild, rev_bndrs')
      | otherwise        = (env',     bndr' : rev_bndrs')
      where
        (env', bndr') = tidyVarBndr env bndr
        env_wild = (occ_env, extendVarEnv subst bndr wild_bndr)
        wild_bndr = setVarName bndr $
                    tidyNameOcc (varName bndr) (mkTyVarOcc "_")
                    -- Tidy the binder to "_"

    is_wildcard :: Var -> Bool
    is_wildcard tv = case occNameString (getOccName tv) of
                       ('_' : rest) -> all isDigit rest
                       _            -> False
274

275
{-
276 277 278 279 280
%************************************************************************
%*                                                                      *
        Destructing coercions
%*                                                                      *
%************************************************************************
281 282 283 284 285 286 287 288 289 290 291

Note [Function coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~
Remember that
  (->) :: forall r1 r2. TYPE r1 -> TYPE r2 -> TYPE LiftedRep

Hence
  FunCo r co1 co2 :: (s1->t1) ~r (s2->t2)
is short for
  TyConAppCo (->) co_rep1 co_rep2 co1 co2
where co_rep1, co_rep2 are the coercions on the representations.
292
-}
batterseapower's avatar
batterseapower committed
293

294

295
-- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
296
-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
batterseapower's avatar
batterseapower committed
297
--
298 299 300 301 302 303 304 305
-- > decomposeCo 3 c [r1, r2, r3] = [nth r1 0 c, nth r2 1 c, nth r3 2 c]
decomposeCo :: Arity -> Coercion
            -> [Role]  -- the roles of the output coercions
                       -- this must have at least as many
                       -- entries as the Arity provided
            -> [Coercion]
decomposeCo arity co rs
  = [mkNthCo r n co | (n,r) <- [0..(arity-1)] `zip` rs ]
306
           -- Remember, Nth is zero-indexed
307

308 309 310 311
decomposeFunCo :: HasDebugCallStack
               => Role      -- Role of the input coercion
               -> Coercion  -- Input coercion
               -> (Coercion, Coercion)
312 313 314
-- Expects co :: (s1 -> t1) ~ (s2 -> t2)
-- Returns (co1 :: s1~s2, co2 :: t1~t2)
-- See Note [Function coercions] for the "2" and "3"
315 316
decomposeFunCo r co = ASSERT2( all_ok, ppr co )
                      (mkNthCo r 2 co, mkNthCo r 3 co)
317 318 319 320
  where
    Pair s1t1 s2t2 = coercionKind co
    all_ok = isFunTy s1t1 && isFunTy s2t2

321 322 323 324 325 326 327 328 329 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
{- Note [Pushing a coercion into a pi-type]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have this:
    (f |> co) t1 .. tn
Then we want to push the coercion into the arguments, so as to make
progress. For example of why you might want to do so, see Note
[Respecting definitional equality] in TyCoRep.

This is done by decomposePiCos.  Specifically, if
    decomposePiCos co [t1,..,tn] = ([co1,...,cok], cor)
then
    (f |> co) t1 .. tn   =   (f (t1 |> co1) ... (tk |> cok)) |> cor) t(k+1) ... tn

Notes:

* k can be smaller than n! That is decomposePiCos can return *fewer*
  coercions than there are arguments (ie k < n), if the kind provided
  doesn't have enough binders.

* If there is a type error, we might see
       (f |> co) t1
  where co :: (forall a. ty) ~ (ty1 -> ty2)
  Here 'co' is insoluble, but we don't want to crash in decoposePiCos.
  So decomposePiCos carefully tests both sides of the coercion to check
  they are both foralls or both arrows.  Not doing this caused Trac #15343.
-}

decomposePiCos :: HasDebugCallStack
               => CoercionN -> Pair Type  -- Coercion and its kind
               -> [Type]
               -> ([CoercionN], CoercionN)
-- See Note [Pushing a coercion into a pi-type]
decomposePiCos orig_co (Pair orig_k1 orig_k2) orig_args
  = go [] (orig_subst,orig_k1) orig_co (orig_subst,orig_k2) orig_args
355
  where
356 357 358 359 360 361 362 363
    orig_subst = mkEmptyTCvSubst $ mkInScopeSet $
                 tyCoVarsOfTypes orig_args `unionVarSet` tyCoVarsOfCo orig_co

    go :: [CoercionN]      -- accumulator for argument coercions, reversed
       -> (TCvSubst,Kind)  -- Lhs kind of coercion
       -> CoercionN        -- coercion originally applied to the function
       -> (TCvSubst,Kind)  -- Rhs kind of coercion
       -> [Type]           -- Arguments to that function
364
       -> ([CoercionN], Coercion)
365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380
    -- Invariant:  co :: subst1(k2) ~ subst2(k2)

    go acc_arg_cos (subst1,k1) co (subst2,k2) (ty:tys)
      | Just (a, t1) <- splitForAllTy_maybe k1
      , Just (b, t2) <- splitForAllTy_maybe k2
        -- know     co :: (forall a:s1.t1) ~ (forall b:s2.t2)
        --    function :: forall a:s1.t1   (the function is not passed to decomposePiCos)
        --           a :: s1
        --           b :: s2
        --          ty :: s2
        -- need arg_co :: s2 ~ s1
        --      res_co :: t1[ty |> arg_co / a] ~ t2[ty / b]
      = let arg_co  = mkNthCo Nominal 0 (mkSymCo co)
            res_co  = mkInstCo co (mkGReflLeftCo Nominal ty arg_co)
            subst1' = extendTCvSubst subst1 a (ty `CastTy` arg_co)
            subst2' = extendTCvSubst subst2 b ty
381
        in
382
        go (arg_co : acc_arg_cos) (subst1', t1) res_co (subst2', t2) tys
383

384 385
      | Just (_s1, t1) <- splitFunTy_maybe k1
      , Just (_s2, t2) <- splitFunTy_maybe k2
386 387 388 389 390
        -- know     co :: (s1 -> t1) ~ (s2 -> t2)
        --    function :: s1 -> t1
        --          ty :: s2
        -- need arg_co :: s2 ~ s1
        --      res_co :: t1 ~ t2
391
      = let (sym_arg_co, res_co) = decomposeFunCo Nominal co
392 393
            arg_co               = mkSymCo sym_arg_co
        in
394
        go (arg_co : acc_arg_cos) (subst1,t1) res_co (subst2,t2) tys
395

396 397 398 399 400
      | not (isEmptyTCvSubst subst1) || not (isEmptyTCvSubst subst2)
      = go acc_arg_cos (zapTCvSubst subst1, substTy subst1 k1)
                       co
                       (zapTCvSubst subst2, substTy subst1 k2)
                       (ty:tys)
401 402 403

      -- tys might not be empty, if the left-hand type of the original coercion
      -- didn't have enough binders
404
    go acc_arg_cos _ki1 co _ki2 _tys = (reverse acc_arg_cos, co)
405

406 407
-- | Attempts to obtain the type variable underlying a 'Coercion'
getCoVar_maybe :: Coercion -> Maybe CoVar
408
getCoVar_maybe (CoVarCo cv) = Just cv
409 410
getCoVar_maybe _            = Nothing

411 412 413
-- | Attempts to tease a coercion apart into a type constructor and the application
-- of a number of coercion arguments to that constructor
splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
Ningning Xie's avatar
Ningning Xie committed
414 415
splitTyConAppCo_maybe co
  | Just (ty, r) <- isReflCo_maybe co
416 417 418 419
  = do { (tc, tys) <- splitTyConApp_maybe ty
       ; let args = zipWith mkReflCo (tyConRolesX r tc) tys
       ; return (tc, args) }
splitTyConAppCo_maybe (TyConAppCo _ tc cos) = Just (tc, cos)
420 421
splitTyConAppCo_maybe (FunCo _ arg res)     = Just (funTyCon, cos)
  where cos = [mkRuntimeRepCo arg, mkRuntimeRepCo res, arg, res]
422 423 424
splitTyConAppCo_maybe _                     = Nothing

-- first result has role equal to input; third result is Nominal
425 426
splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
-- ^ Attempt to take a coercion application apart.
427 428
splitAppCo_maybe (AppCo co arg) = Just (co, arg)
splitAppCo_maybe (TyConAppCo r tc args)
429 430 431 432
  | args `lengthExceeds` tyConArity tc
  , Just (args', arg') <- snocView args
  = Just ( mkTyConAppCo r tc args', arg' )

Simon Peyton Jones's avatar
Simon Peyton Jones committed
433
  | not (mustBeSaturated tc)
434 435
    -- Never create unsaturated type family apps!
  , Just (args', arg') <- snocView args
436
  , Just arg'' <- setNominalRole_maybe (nthRole r tc (length args')) arg'
437
  = Just ( mkTyConAppCo r tc args', arg'' )
438 439
       -- Use mkTyConAppCo to preserve the invariant
       --  that identity coercions are always represented by Refl
440

Ningning Xie's avatar
Ningning Xie committed
441 442 443
splitAppCo_maybe co
  | Just (ty, r) <- isReflCo_maybe co
  , Just (ty1, ty2) <- splitAppTy_maybe ty
444
  = Just (mkReflCo r ty1, mkNomReflCo ty2)
445 446
splitAppCo_maybe _ = Nothing

447 448 449 450
splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
splitFunCo_maybe (FunCo _ arg res) = Just (arg, res)
splitFunCo_maybe _ = Nothing

Ningning Xie's avatar
Ningning Xie committed
451
splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, Coercion, Coercion)
452 453
splitForAllCo_maybe (ForAllCo tv k_co co) = Just (tv, k_co, co)
splitForAllCo_maybe _                     = Nothing
454

Ningning Xie's avatar
Ningning Xie committed
455 456 457 458 459 460 461 462 463 464 465 466
-- | Like 'splitForAllCo_maybe', but only returns Just for tyvar binder
splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
splitForAllCo_ty_maybe (ForAllCo tv k_co co)
  | isTyVar tv = Just (tv, k_co, co)
splitForAllCo_ty_maybe _ = Nothing

-- | Like 'splitForAllCo_maybe', but only returns Just for covar binder
splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
splitForAllCo_co_maybe (ForAllCo cv k_co co)
  | isCoVar cv = Just (cv, k_co, co)
splitForAllCo_co_maybe _ = Nothing

467 468 469
-------------------------------------------------------
-- and some coercion kind stuff

470
coVarTypes :: HasDebugCallStack => CoVar -> Pair Type
471 472
coVarTypes cv
  | (_, _, ty1, ty2, _) <- coVarKindsTypesRole cv
473
  = Pair ty1 ty2
474

475
coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind,Kind,Type,Type,Role)
476 477 478 479 480 481 482 483 484 485 486
coVarKindsTypesRole cv
 | Just (tc, [k1,k2,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
 = let role
         | tc `hasKey` eqPrimTyConKey     = Nominal
         | tc `hasKey` eqReprPrimTyConKey = Representational
         | otherwise                      = panic "coVarKindsTypesRole"
   in (k1,k2,ty1,ty2,role)
 | otherwise = pprPanic "coVarKindsTypesRole, non coercion variable"
                        (ppr cv $$ ppr (varType cv))

coVarKind :: CoVar -> Type
487
coVarKind cv
488 489
  = ASSERT( isCoVar cv )
    varType cv
490

491 492 493 494 495 496 497
coVarRole :: CoVar -> Role
coVarRole cv
  | tc `hasKey` eqPrimTyConKey
  = Nominal
  | tc `hasKey` eqReprPrimTyConKey
  = Representational
  | otherwise
498
  = pprPanic "coVarRole: unknown tycon" (ppr cv <+> dcolon <+> ppr (varType cv))
499 500 501 502 503 504

  where
    tc = case tyConAppTyCon_maybe (varType cv) of
           Just tc0 -> tc0
           Nothing  -> pprPanic "coVarRole: not tyconapp" (ppr cv)

505
-- | Makes a coercion type from two types: the types whose equality
506
-- is proven by the relevant 'Coercion'
507 508 509
mkCoercionType :: Role -> Type -> Type -> Type
mkCoercionType Nominal          = mkPrimEqPred
mkCoercionType Representational = mkReprPrimEqPred
510 511 512 513 514 515 516 517 518 519
mkCoercionType Phantom          = \ty1 ty2 ->
  let ki1 = typeKind ty1
      ki2 = typeKind ty2
  in
  TyConApp eqPhantPrimTyCon [ki1, ki2, ty1, ty2]

mkHeteroCoercionType :: Role -> Kind -> Kind -> Type -> Type -> Type
mkHeteroCoercionType Nominal          = mkHeteroPrimEqPred
mkHeteroCoercionType Representational = mkHeteroReprPrimEqPred
mkHeteroCoercionType Phantom          = panic "mkHeteroCoercionType"
520

521 522
-- | Given a coercion @co1 :: (a :: TYPE r1) ~ (b :: TYPE r2)@,
-- produce a coercion @rep_co :: r1 ~ r2@.
523
mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
524
mkRuntimeRepCo co
525
  = mkNthCo Nominal 0 kind_co
526 527 528 529
  where
    kind_co = mkKindCo co  -- kind_co :: TYPE r1 ~ TYPE r2
                           -- (up to silliness with Constraint)

530
isReflCoVar_maybe :: Var -> Maybe Coercion
531
-- If cv :: t~t then isReflCoVar_maybe cv = Just (Refl t)
532
-- Works on all kinds of Vars, not just CoVars
533
isReflCoVar_maybe cv
534 535
  | isCoVar cv
  , Pair ty1 ty2 <- coVarTypes cv
536
  , ty1 `eqType` ty2
Ningning Xie's avatar
Ningning Xie committed
537
  = Just (mkReflCo (coVarRole cv) ty1)
538 539 540
  | otherwise
  = Nothing

Ningning Xie's avatar
Ningning Xie committed
541 542 543 544 545 546 547 548 549 550 551 552 553 554
-- | Tests if this coercion is obviously a generalized reflexive coercion.
-- Guaranteed to work very quickly.
isGReflCo :: Coercion -> Bool
isGReflCo (GRefl{}) = True
isGReflCo (Refl{})  = True -- Refl ty == GRefl N ty MRefl
isGReflCo _         = False

-- | Tests if this MCoercion is obviously generalized reflexive
-- Guaranteed to work very quickly.
isGReflMCo :: MCoercion -> Bool
isGReflMCo MRefl = True
isGReflMCo (MCo co) | isGReflCo co = True
isGReflMCo _ = False

555 556 557
-- | Tests if this coercion is obviously reflexive. Guaranteed to work
-- very quickly. Sometimes a coercion can be reflexive, but not obviously
-- so. c.f. 'isReflexiveCo'
558
isReflCo :: Coercion -> Bool
Ningning Xie's avatar
Ningning Xie committed
559 560 561 562 563 564 565 566 567 568
isReflCo (Refl{}) = True
isReflCo (GRefl _ _ mco) | isGReflMCo mco = True
isReflCo _ = False

-- | Returns the type coerced if this coercion is a generalized reflexive
-- coercion. Guaranteed to work very quickly.
isGReflCo_maybe :: Coercion -> Maybe (Type, Role)
isGReflCo_maybe (GRefl r ty _) = Just (ty, r)
isGReflCo_maybe (Refl ty)      = Just (ty, Nominal)
isGReflCo_maybe _ = Nothing
569

570 571 572
-- | Returns the type coerced if this coercion is reflexive. Guaranteed
-- to work very quickly. Sometimes a coercion can be reflexive, but not
-- obviously so. c.f. 'isReflexiveCo_maybe'
573
isReflCo_maybe :: Coercion -> Maybe (Type, Role)
Ningning Xie's avatar
Ningning Xie committed
574 575 576
isReflCo_maybe (Refl ty) = Just (ty, Nominal)
isReflCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r)
isReflCo_maybe _ = Nothing
577

578 579 580 581 582 583 584 585
-- | Slowly checks if the coercion is reflexive. Don't call this in a loop,
-- as it walks over the entire coercion.
isReflexiveCo :: Coercion -> Bool
isReflexiveCo = isJust . isReflexiveCo_maybe

-- | Extracts the coerced type from a reflexive coercion. This potentially
-- walks over the entire coercion, so avoid doing this in a loop.
isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
Ningning Xie's avatar
Ningning Xie committed
586 587
isReflexiveCo_maybe (Refl ty) = Just (ty, Nominal)
isReflexiveCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r)
588 589 590 591 592 593 594
isReflexiveCo_maybe co
  | ty1 `eqType` ty2
  = Just (ty1, r)
  | otherwise
  = Nothing
  where (Pair ty1 ty2, r) = coercionKindRole co

595
{-
596 597
%************************************************************************
%*                                                                      *
598
            Building coercions
599 600 601 602 603
%*                                                                      *
%************************************************************************

These "smart constructors" maintain the invariants listed in the definition
of Coercion, and they perform very basic optimizations.
604

605 606 607 608 609 610 611 612 613
Note [Role twiddling functions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

There are a plethora of functions for twiddling roles:

mkSubCo: Requires a nominal input coercion and always produces a
representational output. This is used when you (the programmer) are sure you
know exactly that role you have and what you want.

614
downgradeRole_maybe: This function takes both the input role and the output role
615 616 617 618 619 620 621 622
as parameters. (The *output* role comes first!) It can only *downgrade* a
role -- that is, change it from N to R or P, or from R to P. This one-way
behavior is why there is the "_maybe". If an upgrade is requested, this
function produces Nothing. This is used when you need to change the role of a
coercion, but you're not sure (as you're writing the code) of which roles are
involved.

This function could have been written using coercionRole to ascertain the role
623
of the input. But, that function is recursive, and the caller of downgradeRole_maybe
624 625
often knows the input role. So, this is more efficient.

626 627
downgradeRole: This is just like downgradeRole_maybe, but it panics if the
conversion isn't a downgrade.
628

629 630 631 632 633 634 635 636 637 638
setNominalRole_maybe: This is the only function that can *upgrade* a coercion.
The result (if it exists) is always Nominal. The input can be at any role. It
works on a "best effort" basis, as it should never be strictly necessary to
upgrade a coercion during compilation. It is currently only used within GHC in
splitAppCo_maybe. In order to be a proper inverse of mkAppCo, the second
coercion that splitAppCo_maybe returns must be nominal. But, it's conceivable
that splitAppCo_maybe is operating over a TyConAppCo that uses a
representational coercion. Hence the need for setNominalRole_maybe.
splitAppCo_maybe, in turn, is used only within coercion optimization -- thus,
it is not absolutely critical that setNominalRole_maybe be complete.
639 640 641 642 643 644 645

Note that setNominalRole_maybe will never upgrade a phantom UnivCo. Phantom
UnivCos are perfectly type-safe, whereas representational and nominal ones are
not. Indeed, `unsafeCoerce` is implemented via a representational UnivCo.
(Nominal ones are no worse than representational ones, so this function *will*
change a UnivCo Representational to a UnivCo Nominal.)

646 647 648 649
Conal Elliott also came across a need for this function while working with the
GHC API, as he was decomposing Core casts. The Core casts use representational
coercions, as they must, but his use case required nominal coercions (he was
building a GADT). So, that's why this function is exported from this module.
650

651 652 653
One might ask: shouldn't downgradeRole_maybe just use setNominalRole_maybe as
appropriate? I (Richard E.) have decided not to do this, because upgrading a
role is bizarre and a caller should have to ask for this behavior explicitly.
654

655 656
-}

Ningning Xie's avatar
Ningning Xie committed
657 658 659 660 661 662 663 664
-- | Make a generalized reflexive coercion
mkGReflCo :: Role -> Type -> MCoercionN -> Coercion
mkGReflCo r ty mco
  | isGReflMCo mco = if r == Nominal then Refl ty
                     else GRefl r ty MRefl
  | otherwise    = GRefl r ty mco

-- | Make a reflexive coercion
665
mkReflCo :: Role -> Type -> Coercion
Ningning Xie's avatar
Ningning Xie committed
666 667
mkReflCo Nominal ty = Refl ty
mkReflCo r       ty = GRefl r ty MRefl
668 669 670

-- | Make a representational reflexive coercion
mkRepReflCo :: Type -> Coercion
Ningning Xie's avatar
Ningning Xie committed
671
mkRepReflCo ty = GRefl Representational ty MRefl
672 673 674

-- | Make a nominal reflexive coercion
mkNomReflCo :: Type -> Coercion
Ningning Xie's avatar
Ningning Xie committed
675
mkNomReflCo = Refl
676

677 678
-- | Apply a type constructor to a list of coercions. It is the
-- caller's responsibility to get the roles correct on argument coercions.
679
mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
680
mkTyConAppCo r tc cos
681
  | tc `hasKey` funTyConKey
682
  , [_rep1, _rep2, co1, co2] <- cos   -- See Note [Function coercions]
683 684 685 686 687
  = -- (a :: TYPE ra) -> (b :: TYPE rb)  ~  (c :: TYPE rc) -> (d :: TYPE rd)
    -- rep1 :: ra  ~  rc        rep2 :: rb  ~  rd
    -- co1  :: a   ~  c         co2  :: b   ~  d
    mkFunCo r co1 co2

688
               -- Expand type synonyms
689
  | Just (tv_co_prs, rhs_ty, leftover_cos) <- expandSynTyCon_maybe tc cos
690
  = mkAppCos (liftCoSubst r (mkLiftingContext tv_co_prs) rhs_ty) leftover_cos
691

692
  | Just tys_roles <- traverse isReflCo_maybe cos
Ningning Xie's avatar
Ningning Xie committed
693 694
  = mkReflCo r (mkTyConApp tc (map fst tys_roles))
  -- See Note [Refl invariant]
695

696
  | otherwise = TyConAppCo r tc cos
697

698 699
-- | Build a function 'Coercion' from two other 'Coercion's. That is,
-- given @co1 :: a ~ b@ and @co2 :: x ~ y@ produce @co :: (a -> x) ~ (b -> y)@.
700
mkFunCo :: Role -> Coercion -> Coercion -> Coercion
701 702 703 704
mkFunCo r co1 co2
    -- See Note [Refl invariant]
  | Just (ty1, _) <- isReflCo_maybe co1
  , Just (ty2, _) <- isReflCo_maybe co2
Ningning Xie's avatar
Ningning Xie committed
705
  = mkReflCo r (mkFunTy ty1 ty2)
706
  | otherwise = FunCo r co1 co2
batterseapower's avatar
batterseapower committed
707

708 709 710 711 712 713
-- | Apply a 'Coercion' to another 'Coercion'.
-- The second coercion must be Nominal, unless the first is Phantom.
-- If the first is Phantom, then the second can be either Phantom or Nominal.
mkAppCo :: Coercion     -- ^ :: t1 ~r t2
        -> Coercion     -- ^ :: s1 ~N s2, where s1 :: k1, s2 :: k2
        -> Coercion     -- ^ :: t1 s1 ~r t2 s2
Ningning Xie's avatar
Ningning Xie committed
714 715 716 717
mkAppCo co arg
  | Just (ty1, r) <- isReflCo_maybe co
  , Just (ty2, _) <- isReflCo_maybe arg
  = mkReflCo r (mkAppTy ty1 ty2)
718

Ningning Xie's avatar
Ningning Xie committed
719 720
  | Just (ty1, r) <- isReflCo_maybe co
  , Just (tc, tys) <- splitTyConApp_maybe ty1
721
    -- Expand type synonyms; a TyConAppCo can't have a type synonym (Trac #9102)
722
  = mkTyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
723 724 725 726 727 728 729
  where
    zip_roles (r1:_)  []            = [downgradeRole r1 Nominal arg]
    zip_roles (r1:rs) (ty1:tys)     = mkReflCo r1 ty1 : zip_roles rs tys
    zip_roles _       _             = panic "zip_roles" -- but the roles are infinite...

mkAppCo (TyConAppCo r tc args) arg
  = case r of
730 731
      Nominal          -> mkTyConAppCo Nominal tc (args ++ [arg])
      Representational -> mkTyConAppCo Representational tc (args ++ [arg'])
732
        where new_role = (tyConRolesRepresentational tc) !! (length args)
733
              arg'     = downgradeRole new_role Nominal arg
734
      Phantom          -> mkTyConAppCo Phantom tc (args ++ [toPhantomCo arg])
735 736 737 738 739 740 741 742 743 744
mkAppCo co arg = AppCo co  arg
-- Note, mkAppCo is careful to maintain invariants regarding
-- where Refl constructors appear; see the comments in the definition
-- of Coercion and the Note [Refl invariant] in TyCoRep.

-- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
-- See also 'mkAppCo'.
mkAppCos :: Coercion
         -> [Coercion]
         -> Coercion
745
mkAppCos co1 cos = foldl' mkAppCo co1 cos
746

Ningning Xie's avatar
Ningning Xie committed
747
{- Note [Unused coercion variable in ForAllCo]
748

Ningning Xie's avatar
Ningning Xie committed
749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764
See Note [Unused coercion variable in ForAllTy] in TyCoRep for the motivation for
checking coercion variable in types.
To lift the design choice to (ForAllCo cv kind_co body_co), we have two options:

(1) In mkForAllCo, we check whether cv is a coercion variable
    and whether it is not used in body_co. If so we construct a FunCo.
(2) We don't do this check in mkForAllCo.
    In coercionKind, we use mkTyCoForAllTy to perform the check and construct
    a FunTy when necessary.

We chose (2) for two reasons:

* for a coercion, all that matters is its kind, So ForAllCo or FunCo does not
  make a difference.
* even if cv occurs in body_co, it is possible that cv does not occur in the kind
  of body_co. Therefore the check in coercionKind is inevitable.
765

766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782
The last wrinkle is that there are restrictions around the use of the cv in the
coercion, as described in Section 5.8.5.2 of Richard's thesis. The idea is that
we cannot prove that the type system is consistent with unrestricted use of this
cv; the consistency proof uses an untyped rewrite relation that works over types
with all coercions and casts removed. So, we can allow the cv to appear only in
positions that are erased. As an approximation of this (and keeping close to the
published theory), we currently allow the cv only within the type in a Refl node
and under a GRefl node (including in the Coercion stored in a GRefl). It's
possible other places are OK, too, but this is a safe approximation.

Sadly, with heterogeneous equality, this restriction might be able to be violated;
Richard's thesis is unable to prove that it isn't. Specifically, the liftCoSubst
function might create an invalid coercion. Because a violation of the
restriction might lead to a program that "goes wrong", it is checked all the time,
even in a production compiler and without -dcore-list. We *have* proved that the
problem does not occur with homogeneous equality, so this check can be dropped
once ~# is made to be homogeneous.
Ningning Xie's avatar
Ningning Xie committed
783 784 785 786 787 788 789
-}


-- | Make a Coercion from a tycovar, a kind coercion, and a body coercion.
-- The kind of the tycovar should be the left-hand kind of the kind coercion.
-- See Note [Unused coercion variable in ForAllCo]
mkForAllCo :: TyCoVar -> CoercionN -> Coercion -> Coercion
790 791 792
mkForAllCo v kind_co co
  | ASSERT( varType v `eqType` (pFst $ coercionKind kind_co)) True
  , ASSERT( isTyVar v || almostDevoidCoVarOfCo v co) True
Ningning Xie's avatar
Ningning Xie committed
793
  , Just (ty, r) <- isReflCo_maybe co
Ningning Xie's avatar
Ningning Xie committed
794
  , isGReflCo kind_co
795
  = mkReflCo r (mkTyCoInvForAllTy v ty)
Ningning Xie's avatar
Ningning Xie committed
796
  | otherwise
797
  = ForAllCo v kind_co co
Ningning Xie's avatar
Ningning Xie committed
798 799 800 801 802

-- | Like 'mkForAllCo', but the inner coercion shouldn't be an obvious
-- reflexive coercion. For example, it is guaranteed in 'mkForAllCos'.
-- The kind of the tycovar should be the left-hand kind of the kind coercion.
mkForAllCo_NoRefl :: TyCoVar -> CoercionN -> Coercion -> Coercion
803 804 805
mkForAllCo_NoRefl v kind_co co
  | ASSERT( varType v `eqType` (pFst $ coercionKind kind_co)) True
  , ASSERT( isTyVar v || almostDevoidCoVarOfCo v co) True
Ningning Xie's avatar
Ningning Xie committed
806
  , ASSERT( not (isReflCo co)) True
807 808
  , isCoVar v
  , not (v `elemVarSet` tyCoVarsOfCo co)
Ningning Xie's avatar
Ningning Xie committed
809
  = FunCo (coercionRole co) kind_co co
810
  | otherwise
811
  = ForAllCo v kind_co co
812 813

-- | Make nested ForAllCos
Ningning Xie's avatar
Ningning Xie committed
814
mkForAllCos :: [(TyCoVar, CoercionN)] -> Coercion -> Coercion
Ningning Xie's avatar
Ningning Xie committed
815 816
mkForAllCos bndrs co
  | Just (ty, r ) <- isReflCo_maybe co
817
  = let (refls_rev'd, non_refls_rev'd) = span (isReflCo . snd) (reverse bndrs) in
Ningning Xie's avatar
Ningning Xie committed
818 819
    foldl' (flip $ uncurry mkForAllCo_NoRefl)
           (mkReflCo r (mkTyCoInvForAllTys (reverse (map fst refls_rev'd)) ty))
820
           non_refls_rev'd
Ningning Xie's avatar
Ningning Xie committed
821
  | otherwise
Ningning Xie's avatar
Ningning Xie committed
822
  = foldr (uncurry mkForAllCo_NoRefl) co bndrs
823

Ningning Xie's avatar
Ningning Xie committed
824
-- | Make a Coercion quantified over a type/coercion variable;
825
-- the variable has the same type in both sides of the coercion
Ningning Xie's avatar
Ningning Xie committed
826
mkHomoForAllCos :: [TyCoVar] -> Coercion -> Coercion
827
mkHomoForAllCos vs co
Ningning Xie's avatar
Ningning Xie committed
828
  | Just (ty, r) <- isReflCo_maybe co
829
  = mkReflCo r (mkTyCoInvForAllTys vs ty)
Ningning Xie's avatar
Ningning Xie committed
830
  | otherwise
831
  = mkHomoForAllCos_NoRefl vs co
832

Ningning Xie's avatar
Ningning Xie committed
833 834 835
-- | Like 'mkHomoForAllCos', but the inner coercion shouldn't be an obvious
-- reflexive coercion. For example, it is guaranteed in 'mkHomoForAllCos'.
mkHomoForAllCos_NoRefl :: [TyCoVar] -> Coercion -> Coercion
836
mkHomoForAllCos_NoRefl vs orig_co
Ningning Xie's avatar
Ningning Xie committed
837
  = ASSERT( not (isReflCo orig_co))
838
    foldr go orig_co vs
839
  where
840
    go v co = mkForAllCo_NoRefl v (mkNomReflCo (varType v)) co
841 842 843

mkCoVarCo :: CoVar -> Coercion
-- cv :: s ~# t
844 845
-- See Note [mkCoVarCo]
mkCoVarCo cv = CoVarCo cv
846 847 848 849

mkCoVarCos :: [CoVar] -> [Coercion]
mkCoVarCos = map mkCoVarCo

850 851 852 853 854 855 856 857
{- Note [mkCoVarCo]
~~~~~~~~~~~~~~~~~~~
In the past, mkCoVarCo optimised (c :: t~t) to (Refl t).  That is
valid (although see Note [Unbound RULE binders] in Rules), but
it's a relatively expensive test and perhaps better done in
optCoercion.  Not a big deal either way.
-}

858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888
-- | Extract a covar, if possible. This check is dirty. Be ashamed
-- of yourself. (It's dirty because it cares about the structure of
-- a coercion, which is morally reprehensible.)
isCoVar_maybe :: Coercion -> Maybe CoVar
isCoVar_maybe (CoVarCo cv) = Just cv
isCoVar_maybe _            = Nothing

mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> [Coercion]
           -> Coercion
-- mkAxInstCo can legitimately be called over-staturated;
-- i.e. with more type arguments than the coercion requires
mkAxInstCo role ax index tys cos
  | arity == n_tys = downgradeRole role ax_role $
                     mkAxiomInstCo ax_br index (rtys `chkAppend` cos)
  | otherwise      = ASSERT( arity < n_tys )
                     downgradeRole role ax_role $
                     mkAppCos (mkAxiomInstCo ax_br index
                                             (ax_args `chkAppend` cos))
                              leftover_args
  where
    n_tys         = length tys
    ax_br         = toBranchedAxiom ax
    branch        = coAxiomNthBranch ax_br index
    tvs           = coAxBranchTyVars branch
    arity         = length tvs
    arg_roles     = coAxBranchRoles branch
    rtys          = zipWith mkReflCo (arg_roles ++ repeat Nominal) tys
    (ax_args, leftover_args)
                  = splitAt arity rtys
    ax_role       = coAxiomRole ax

Ningning Xie's avatar
Ningning Xie committed
889
-- worker function
890 891
mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
mkAxiomInstCo ax index args
892
  = ASSERT( args `lengthIs` coAxiomArity ax index )
893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949
    AxiomInstCo ax index args

-- to be used only with unbranched axioms
mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched
                     -> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo role ax tys cos
  = mkAxInstCo role ax 0 tys cos

mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
-- Instantiate the axiom with specified types,
-- returning the instantiated RHS
-- A companion to mkAxInstCo:
--    mkAxInstRhs ax index tys = snd (coercionKind (mkAxInstCo ax index tys))
mkAxInstRHS ax index tys cos
  = ASSERT( tvs `equalLength` tys1 )
    mkAppTys rhs' tys2
  where
    branch       = coAxiomNthBranch ax index
    tvs          = coAxBranchTyVars branch
    cvs          = coAxBranchCoVars branch
    (tys1, tys2) = splitAtList tvs tys
    rhs'         = substTyWith tvs tys1 $
                   substTyWithCoVars cvs cos $
                   coAxBranchRHS branch

mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
mkUnbranchedAxInstRHS ax = mkAxInstRHS ax 0

-- | Return the left-hand type of the axiom, when the axiom is instantiated
-- at the types given.
mkAxInstLHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
mkAxInstLHS ax index tys cos
  = ASSERT( tvs `equalLength` tys1 )
    mkTyConApp fam_tc (lhs_tys `chkAppend` tys2)
  where
    branch       = coAxiomNthBranch ax index
    tvs          = coAxBranchTyVars branch
    cvs          = coAxBranchCoVars branch
    (tys1, tys2) = splitAtList tvs tys
    lhs_tys      = substTysWith tvs tys1 $
                   substTysWithCoVars cvs cos $
                   coAxBranchLHS branch
    fam_tc       = coAxiomTyCon ax

-- | Instantiate the left-hand side of an unbranched axiom
mkUnbranchedAxInstLHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
mkUnbranchedAxInstLHS ax = mkAxInstLHS ax 0

-- | Manufacture an unsafe coercion from thin air.
--   Currently (May 14) this is used only to implement the
--   @unsafeCoerce#@ primitive.  Optimise by pushing
--   down through type constructors.
mkUnsafeCo :: Role -> Type -> Type -> Coercion
mkUnsafeCo role ty1 ty2
  = mkUnivCo UnsafeCoerceProv role ty1 ty2

-- | Make a coercion from a coercion hole
Simon Peyton Jones's avatar
Simon Peyton Jones committed
950 951
mkHoleCo :: CoercionHole -> Coercion
mkHoleCo h = HoleCo h
952 953 954 955 956 957 958 959

-- | Make a universal coercion between two arbitrary types.
mkUnivCo :: UnivCoProvenance
         -> Role       -- ^ role of the built coercion, "r"
         -> Type       -- ^ t1 :: k1
         -> Type       -- ^ t2 :: k2
         -> Coercion   -- ^ :: t1 ~r t2
mkUnivCo prov role ty1 ty2
Ningning Xie's avatar
Ningning Xie committed
960
  | ty1 `eqType` ty2 = mkReflCo role ty1
961
  | otherwise        = UnivCo prov role ty1 ty2
batterseapower's avatar
batterseapower committed
962

963 964 965 966 967 968 969
-- | Create a symmetric version of the given 'Coercion' that asserts
--   equality between the same types but in the other "direction", so
--   a kind of @t1 ~ t2@ becomes the kind @t2 ~ t1@.
mkSymCo :: Coercion -> Coercion

-- Do a few simple optimizations, but don't bother pushing occurrences
-- of symmetry to the leaves; the optimizer will take care of that.
Ningning Xie's avatar
Ningning Xie committed
970
mkSymCo co | isReflCo co          = co
971 972 973
mkSymCo    (SymCo co)             = co
mkSymCo    (SubCo (SymCo co))     = SubCo co
mkSymCo co                        = SymCo co
974 975

-- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
976
--   (co1 ; co2)
977
mkTransCo :: Coercion -> Coercion -> Coercion
Ningning Xie's avatar
Ningning Xie committed
978 979 980 981 982
mkTransCo co1 co2 | isReflCo co1 = co2
                  | isReflCo co2 = co1
mkTransCo (GRefl r t1 (MCo co1)) (GRefl _ _ (MCo co2))
  = GRefl r t1 (MCo $ mkTransCo co1 co2)
mkTransCo co1 co2                 = TransCo co1 co2
983

984 985 986 987 988 989
-- | Compose two MCoercions via transitivity
mkTransMCo :: MCoercion -> MCoercion -> MCoercion
mkTransMCo MRefl     co2       = co2
mkTransMCo co1       MRefl     = co1
mkTransMCo (MCo co1) (MCo co2) = MCo (mkTransCo co1 co2)

990
mkNthCo :: HasDebugCallStack
991 992
        => Role  -- The role of the coercion you're creating
        -> Int   -- Zero-indexed
993 994 995
        -> Coercion
        -> Coercion
mkNthCo r n co
996
  = ASSERT2( good_call, bad_call_msg )
997 998 999 1000
    go r n co
  where
    Pair ty1 ty2 = coercionKind co

Ningning Xie's avatar
Ningning Xie committed
1001 1002 1003
    go r 0 co
      | Just (ty, _) <- isReflCo_maybe co
      , Just (tv, _) <- splitForAllTy_maybe ty
Ningning Xie's avatar
Ningning Xie committed
1004 1005 1006
      = -- works for both tyvar and covar
        ASSERT( r == Nominal )
        mkNomReflCo (varType tv)
Ningning Xie's avatar
Ningning Xie committed
1007 1008 1009 1010

    go r n co
      | Just (ty, r0) <- isReflCo_maybe co
      , let tc = tyConAppTyCon ty
1011 1012 1013
      = ASSERT2( ok_tc_app ty n, ppr n $$ ppr ty )
        ASSERT( nthRole r0 tc n == r )
        mkReflCo r (tyConAppArgN n ty)
Ningning Xie's avatar
Ningning Xie committed
1014
      where ok_tc_app :: Type -> Int -> Bool
1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027
            ok_tc_app ty n
              | Just (_, tys) <- splitTyConApp_maybe ty
              = tys `lengthExceeds` n
              | isForAllTy ty  -- nth:0 pulls out a kind coercion from a hetero forall
              = n == 0
              | otherwise
              = False

    go r 0 (ForAllCo _ kind_co _)
      = ASSERT( r == Nominal )
        kind_co
      -- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2)
      -- then (nth 0 co :: k1 ~N k2)
Ningning Xie's avatar
Ningning Xie committed
1028 1029
      -- If co :: (forall a1:t1 ~ t2. t1) ~ (forall a2:t3 ~ t4. t2)
      -- then (nth 0 co :: (t1 ~ t2) ~N (t3 ~ t4))
1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058

    go r n co@(FunCo r0 arg res)
      -- See Note [Function coercions]
      -- If FunCo _ arg_co res_co ::   (s1:TYPE sk1 -> s2:TYPE sk2)
      --                             ~ (t1:TYPE tk1 -> t2:TYPE tk2)
      -- Then we want to behave as if co was
      --    TyConAppCo argk_co resk_co arg_co res_co
      -- where
      --    argk_co :: sk1 ~ tk1  =  mkNthCo 0 (mkKindCo arg_co)
      --    resk_co :: sk2 ~ tk2  =  mkNthCo 0 (mkKindCo res_co)
      --                             i.e. mkRuntimeRepCo
      = case n of
          0 -> ASSERT( r == Nominal ) mkRuntimeRepCo arg
          1 -> ASSERT( r == Nominal ) mkRuntimeRepCo res
          2 -> ASSERT( r == r0 )      arg
          3 -> ASSERT( r == r0 )      res
          _ -> pprPanic "mkNthCo(FunCo)" (ppr n $$ ppr co)

    go r n (TyConAppCo r0 tc arg_cos) = ASSERT2( r == nthRole r0 tc n
                                                    , (vcat [ ppr tc
                                                            , ppr arg_cos
                                                            , ppr r0
                                                            , ppr n
                                                            , ppr r ]) )
                                             arg_cos `getNth` n

    go r n co =
      NthCo r n co

1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099
    -- Assertion checking
    bad_call_msg = vcat [ text "Coercion =" <+> ppr co
                        , text "LHS ty =" <+> ppr ty1
                        , text "RHS ty =" <+> ppr ty2
                        , text "n =" <+> ppr n, text "r =" <+> ppr r
                        , text "coercion role =" <+> ppr (coercionRole co) ]
    good_call
      -- If the Coercion passed in is between forall-types, then the Int must
      -- be 0 and the role must be Nominal.
      | Just (_tv1, _) <- splitForAllTy_maybe ty1
      , Just (_tv2, _) <- splitForAllTy_maybe ty2
      = n == 0 && r == Nominal

      -- If the Coercion passed in is between T tys and T tys', then the Int
      -- must be less than the length of tys/tys' (which must be the same
      -- lengths).
      --
      -- If the role of the Coercion is nominal, then the role passed in must
      -- be nominal. If the role of the Coercion is representational, then the
      -- role passed in must be tyConRolesRepresentational T !! n. If the role
      -- of the Coercion is Phantom, then the role passed in must be Phantom.
      --
      -- See also Note [NthCo Cached Roles] if you're wondering why it's
      -- blaringly obvious that we should be *computing* this role instead of
      -- passing it in.
      | Just (tc1, tys1) <- splitTyConApp_maybe ty1
      , Just (tc2, tys2) <- splitTyConApp_maybe ty2
      , tc1 == tc2
      = let len1 = length tys1
            len2 = length tys2
            good_role = case coercionRole co of
                          Nominal -> r == Nominal
                          Representational -> r == (tyConRolesRepresentational tc1 !! n)
                          Phantom -> r == Phantom
        in len1 == len2 && n < len1 && good_role

      | otherwise
      = True



1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114
-- | If you're about to call @mkNthCo r n co@, then @r@ should be
-- whatever @nthCoRole n co@ returns.
nthCoRole :: Int -> Coercion -> Role
nthCoRole n co
  | Just (tc, _) <- splitTyConApp_maybe lty
  = nthRole r tc n

  | Just _ <- splitForAllTy_maybe lty
  = Nominal

  | otherwise
  = pprPanic "nthCoRole" (ppr co)

  where
    (Pair lty _, r) = coercionKindRole co
1115

1116
mkLRCo :: LeftOrRight -> Coercion -> Coercion
Ningning Xie's avatar
Ningning Xie committed
1117 1118 1119 1120 1121
mkLRCo lr co
  | Just (ty, eq) <- isReflCo_maybe co
  = mkReflCo eq (pickLR lr (splitAppTy ty))
  | otherwise
  = LRCo lr co
1122

1123 1124
-- | Instantiates a 'Coercion'.
mkInstCo :: Coercion -> Coercion -> Coercion
Ningning Xie's avatar
Ningning Xie committed
1125
mkInstCo (ForAllCo tcv _kind_co body_co) co
Ningning Xie's avatar
Ningning Xie committed
1126
  | Just (arg, _) <- isReflCo_maybe co
Ningning Xie's avatar
Ningning Xie committed
1127 1128
      -- works for both tyvar and covar
  = substCoUnchecked (zipTCvSubst [tcv] [arg]) body_co
1129 1130
mkInstCo co arg = InstCo co arg

Ningning Xie's avatar
Ningning Xie committed
1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148
-- | Given @ty :: k1@, @co :: k1 ~ k2@,
-- produces @co' :: ty ~r (ty |> co)@
mkGReflRightCo :: Role -> Type -> CoercionN -> Coercion
mkGReflRightCo r ty co
  | isGReflCo co = mkReflCo r ty
    -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@
    -- instead of @isReflCo@
  | otherwise = GRefl r ty (MCo co)

-- | Given @ty :: k1@, @co :: k1 ~ k2@,
-- produces @co' :: (ty |> co) ~r ty@
mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion
mkGReflLeftCo r ty co
  | isGReflCo co = mkReflCo r ty
    -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@
    -- instead of @isReflCo@
  | otherwise    = mkSymCo $ GRefl r ty (MCo co)

1149
-- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty ~r ty'@,
Ningning Xie's avatar
Ningning Xie committed
1150 1151 1152 1153 1154 1155 1156 1157
-- produces @co' :: (ty |> co) ~r ty'
-- It is not only a utility function, but it saves allocation when co
-- is a GRefl coercion.
mkCoherenceLeftCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
mkCoherenceLeftCo r ty co co2
  | isGReflCo co = co2
  | otherwise = (mkSymCo $ GRefl r ty (MCo co)) `mkTransCo` co2

1158
-- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty' ~r ty@,
Ningning Xie's avatar
Ningning Xie committed
1159 1160 1161 1162 1163 1164 1165
-- produces @co' :: ty' ~r (ty |> co)
-- It is not only a utility function, but it saves allocation when co
-- is a GRefl coercion.
mkCoherenceRightCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
mkCoherenceRightCo r ty co co2
  | isGReflCo co = co2
  | otherwise = co2 `mkTransCo` GRefl r ty (MCo co)
1166

1167
-- | Given @co :: (a :: k) ~ (b :: k')@ produce @co' :: k ~ k'@.
1168
mkKindCo :: Coercion -> Coercion
Ningning Xie's avatar
Ningning Xie committed
1169 1170
mkKindCo co | Just (ty, _) <- isReflCo_maybe co = Refl (typeKind ty)
mkKindCo (GRefl _ _ (MCo co)) = co
1171 1172 1173 1174 1175 1176 1177
mkKindCo (UnivCo (PhantomProv h) _ _ _)    = h
mkKindCo (UnivCo (ProofIrrelProv h) _ _ _) = h
mkKindCo co
  | Pair ty1 ty2 <- coercionKind co
       -- generally, calling coercionKind during coercion creation is a bad idea,
       -- as it can lead to exponential behavior. But, we don't have nested mkKindCos,
       -- so it's OK here.
1178 1179 1180
  , let tk1 = typeKind ty1
        tk2 = typeKind ty2
  , tk1 `eqType` tk2
Ningning Xie's avatar
Ningning Xie committed
1181
  = Refl tk1
1182 1183
  | otherwise
  = KindCo co
1184

1185
mkSubCo :: Coercion -> Coercion
1186 1187
-- Input coercion is Nominal, result is Representational
-- see also Note [Role twiddling functions]
Ningning Xie's avatar
Ningning Xie committed
1188 1189
mkSubCo (Refl ty) = GRefl Representational ty MRefl
mkSubCo (GRefl Nominal ty co) = GRefl Representational ty co
1190 1191
mkSubCo (TyConAppCo Nominal tc cos)
  = TyConAppCo Representational tc (applyRoles tc cos)
1192 1193 1194 1195
mkSubCo (FunCo Nominal arg res)
  = FunCo Representational
          (downgradeRole Representational Nominal arg)
          (downgradeRole Representational Nominal res)
Joachim Breitner's avatar
Joachim Breitner committed
1196
mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
1197 1198
             SubCo co

1199 1200 1201 1202
-- | Changes a role, but only a downgrade. See Note [Role twiddling functions]
downgradeRole_maybe :: Role   -- ^ desired role
                    -> Role   -- ^ current role
                    -> Coercion -> Maybe Coercion
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1203 1204
-- In (downgradeRole_maybe dr cr co) it's a precondition that
--                                   cr = coercionRole co
1205 1206 1207 1208 1209 1210 1211 1212 1213 1214

downgradeRole_maybe Nominal          Nominal          co = Just co
downgradeRole_maybe Nominal          _                _  = Nothing

downgradeRole_maybe Representational Nominal          co = Just (mkSubCo co)
downgradeRole_maybe Representational Representational co = Just co
downgradeRole_maybe Representational Phantom          _  = Nothing

downgradeRole_maybe Phantom          Phantom          co = Just co
downgradeRole_maybe Phantom          _                co = Just (toPhantomCo co)