    {-# OPTIONS_GHC -Wno-orphans     #-} -- Outputable
    {-# LANGUAGE DataKinds           #-}
    {-# LANGUAGE DeriveDataTypeable  #-}
    {-# LANGUAGE GADTs               #-}
    {-# LANGUAGE KindSignatures      #-}
    {-# LANGUAGE RoleAnnotations     #-}
    {-# LANGUAGE ScopedTypeVariables #-}

    -- (c) The University of Glasgow 2012

    -- | Module for coercion axioms, used to represent type family instances
    -- and newtypes

    module GHC.Core.Coercion.Axiom (
           BranchFlag, Branched, Unbranched, BranchIndex, Branches(..),
           manyBranches, unbranched,
           fromBranches, numBranches,
           mapAccumBranches,

           CoAxiom(..), CoAxBranch(..),

           toBranchedAxiom, toUnbranchedAxiom,
           coAxiomName, coAxiomArity, coAxiomBranches,
           coAxiomTyCon, isImplicitCoAxiom, coAxiomNumPats,
           coAxiomNthBranch, coAxiomSingleBranch_maybe, coAxiomRole,
           coAxiomSingleBranch, coAxBranchTyVars, coAxBranchCoVars,
           coAxBranchRoles,
           coAxBranchLHS, coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps,
           placeHolderIncomps,

           Role(..), fsFromRole,

           CoAxiomRule(..), BuiltInFamRewrite(..), BuiltInFamInjectivity(..), TypeEqn,
           coAxiomRuleArgRoles, coAxiomRuleRole,
           coAxiomRuleBranch_maybe, isNewtypeAxiomRule_maybe,
           BuiltInSynFamily(..), trivialBuiltInFamily
           ) where

    import GHC.Prelude

    import Language.Haskell.Syntax.Basic (Role(..))

    import {-# SOURCE #-} GHC.Core.TyCo.Rep ( Type )
    import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprType, pprTyVar )
    import {-# SOURCE #-} GHC.Core.TyCon    ( TyCon, isNewTyCon )
    import GHC.Utils.Outputable
    import GHC.Data.FastString
    import GHC.Types.Name
    import GHC.Types.Unique
    import GHC.Types.Var
    import GHC.Utils.Misc
    import GHC.Utils.Binary
    import GHC.Utils.Panic
    import GHC.Data.Pair
    import GHC.Types.Basic
    import Data.Typeable ( Typeable )
    import GHC.Types.SrcLoc
    import qualified Data.Data as Data
    import Data.Array
    import Data.List ( mapAccumL )

    {-
    Note [Coercion axiom branches]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    In order to allow closed type families, an axiom needs to contain an
    ordered list of alternatives, called branches. The kind of the coercion built
    from an axiom is determined by which index is used when building the coercion
    from the axiom.

    For example, consider the axiom derived from the following declaration:

    type family F a where
      F [Int] = Bool
      F [a]   = Double
      F (a b) = Char

    This will give rise to this axiom:

    axF :: {                                         F [Int] ~ Bool
           ; forall (a :: *).                        F [a]   ~ Double
           ; forall (k :: *) (a :: k -> *) (b :: k). F (a b) ~ Char
           }

    The axiom is used with the AxiomCo constructor of Coercion. If we wish
    to have a coercion showing that F (Maybe Int) ~ Char, it will look like

    axF[2] <*> <Maybe> <Int> :: F (Maybe Int) ~ Char
    -- or, written using concrete-ish syntax --
    AxiomRuleCo axF 2 [Refl *, Refl Maybe, Refl Int]

    Note that the index is 0-based.

    For type-checking, it is also necessary to check that no previous pattern
    can unify with the supplied arguments. After all, it is possible that some
    of the type arguments are lambda-bound type variables whose instantiation may
    cause an earlier match among the branches. We wish to prohibit this behavior,
    so the type checker rules out the choice of a branch where a previous branch
    can unify. See also [Apartness] in GHC.Core.FamInstEnv.

    For example, the following is malformed, where 'a' is a lambda-bound type
    variable:

    axF[2] <*> <a> <Bool> :: F (a Bool) ~ Char

    Why? Because a might be instantiated with [], meaning that branch 1 should
    apply, not branch 2. This is a vital consistency check; without it, we could
    derive Int ~ Bool, and that is a Bad Thing.

    Note [Branched axioms]
    ~~~~~~~~~~~~~~~~~~~~~~
    Although a CoAxiom has the capacity to store many branches, in certain cases,
    we want only one. These cases are in data/newtype family instances, newtype
    coercions, and type family instances.
    Furthermore, these unbranched axioms are used in a
    variety of places throughout GHC, and it would difficult to generalize all of
    that code to deal with branched axioms, especially when the code can be sure
    of the fact that an axiom is indeed a singleton. At the same time, it seems
    dangerous to assume singlehood in various places through GHC.

    The solution to this is to label a CoAxiom with a phantom type variable
    declaring whether it is known to be a singleton or not. The branches
    are stored using a special datatype, declared below, that ensures that the
    type variable is accurate.

    ************************************************************************
    *                                                                      *
                        Branches
    *                                                                      *
    ************************************************************************
    -}

    {- Note [BranchIndex]
    ~~~~~~~~~~~~~~~~~~~~
    A CoAxiom has 1 or more branches. Each branch has contains a list
    of the free type variables in that branch, the LHS type patterns,
    and the RHS type for that branch. When we apply an axiom to a list
    of coercions, we must choose which branch of the axiom we wish to
    use, as the different branches may have different numbers of free
    type variables. (The number of type patterns is always the same
    among branches, but that doesn't quite concern us here.)
    -}

    type BranchIndex = Int         -- Counting from zero
          -- The index of the branch in the list of branches
          -- See Note [BranchIndex]

    -- promoted data type
    data BranchFlag = Branched | Unbranched
    type Branched = 'Branched
    type Unbranched = 'Unbranched
    -- By using type synonyms for the promoted constructors, we avoid needing
    -- DataKinds and the promotion quote in client modules. This also means that
    -- we don't need to export the term-level constructors, which should never be used.

    newtype Branches (br :: BranchFlag)
      = MkBranches { forall (br :: BranchFlag).
    Branches br -> Array BranchIndex CoAxBranch
    unMkBranches :: Array BranchIndex CoAxBranch }
    type role Branches nominal

    manyBranches :: [CoAxBranch] -> Branches Branched
    manyBranches :: [CoAxBranch] -> Branches Branched
    manyBranches [CoAxBranch]
    brs = Bool
    -> (Array BranchIndex CoAxBranch -> Branches Branched)
    -> Array BranchIndex CoAxBranch
    -> Branches Branched
    forall a. HasCallStack => Bool -> a -> a
    assert ((BranchIndex, BranchIndex) -> BranchIndex
    forall a b. (a, b) -> b
    snd (BranchIndex, BranchIndex)
    bnds BranchIndex -> BranchIndex -> Bool
    forall a. Ord a => a -> a -> Bool
    >= (BranchIndex, BranchIndex) -> BranchIndex
    forall a b. (a, b) -> a
    fst (BranchIndex, BranchIndex)
    bnds )
                       Array BranchIndex CoAxBranch -> Branches Branched
    forall (br :: BranchFlag).
    Array BranchIndex CoAxBranch -> Branches br
    MkBranches ((BranchIndex, BranchIndex)
    -> [CoAxBranch] -> Array BranchIndex CoAxBranch
    forall i e. Ix i => (i, i) -> [e] -> Array i e
    listArray (BranchIndex, BranchIndex)
    bnds [CoAxBranch]
    brs)
      where
        bnds :: (BranchIndex, BranchIndex)
    bnds = (BranchIndex
    0, [CoAxBranch] -> BranchIndex
    forall a. [a] -> BranchIndex
    forall (t :: * -> *) a. Foldable t => t a -> BranchIndex
    length [CoAxBranch]
    brs BranchIndex -> BranchIndex -> BranchIndex
    forall a. Num a => a -> a -> a
    - BranchIndex
    1)

    unbranched :: CoAxBranch -> Branches Unbranched
    unbranched :: CoAxBranch -> Branches Unbranched
    unbranched CoAxBranch
    br = Array BranchIndex CoAxBranch -> Branches Unbranched
    forall (br :: BranchFlag).
    Array BranchIndex CoAxBranch -> Branches br
    MkBranches ((BranchIndex, BranchIndex)
    -> [CoAxBranch] -> Array BranchIndex CoAxBranch
    forall i e. Ix i => (i, i) -> [e] -> Array i e
    listArray (BranchIndex
    0, BranchIndex
    0) [CoAxBranch
    br])

    toBranched :: Branches br -> Branches Branched
    toBranched :: forall (br :: BranchFlag). Branches br -> Branches Branched
    toBranched = Array BranchIndex CoAxBranch -> Branches Branched
    forall (br :: BranchFlag).
    Array BranchIndex CoAxBranch -> Branches br
    MkBranches (Array BranchIndex CoAxBranch -> Branches Branched)
    -> (Branches br -> Array BranchIndex CoAxBranch)
    -> Branches br
    -> Branches Branched
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Branches br -> Array BranchIndex CoAxBranch
    forall (br :: BranchFlag).
    Branches br -> Array BranchIndex CoAxBranch
    unMkBranches

    toUnbranched :: Branches br -> Branches Unbranched
    toUnbranched :: forall (br :: BranchFlag). Branches br -> Branches Unbranched
    toUnbranched (MkBranches Array BranchIndex CoAxBranch
    arr) = Bool
    -> (Array BranchIndex CoAxBranch -> Branches Unbranched)
    -> Array BranchIndex CoAxBranch
    -> Branches Unbranched
    forall a. HasCallStack => Bool -> a -> a
    assert (Array BranchIndex CoAxBranch -> (BranchIndex, BranchIndex)
    forall i e. Array i e -> (i, i)
    bounds Array BranchIndex CoAxBranch
    arr (BranchIndex, BranchIndex) -> (BranchIndex, BranchIndex) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (BranchIndex
    0,BranchIndex
    0) )
                                    Array BranchIndex CoAxBranch -> Branches Unbranched
    forall (br :: BranchFlag).
    Array BranchIndex CoAxBranch -> Branches br
    MkBranches Array BranchIndex CoAxBranch
    arr

    fromBranches :: Branches br -> [CoAxBranch]
    fromBranches :: forall (br :: BranchFlag). Branches br -> [CoAxBranch]
    fromBranches = Array BranchIndex CoAxBranch -> [CoAxBranch]
    forall i e. Array i e -> [e]
    elems (Array BranchIndex CoAxBranch -> [CoAxBranch])
    -> (Branches br -> Array BranchIndex CoAxBranch)
    -> Branches br
    -> [CoAxBranch]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Branches br -> Array BranchIndex CoAxBranch
    forall (br :: BranchFlag).
    Branches br -> Array BranchIndex CoAxBranch
    unMkBranches

    branchesNth :: Branches br -> BranchIndex -> CoAxBranch
    branchesNth :: forall (br :: BranchFlag). Branches br -> BranchIndex -> CoAxBranch
    branchesNth (MkBranches Array BranchIndex CoAxBranch
    arr) BranchIndex
    n = Array BranchIndex CoAxBranch
    arr Array BranchIndex CoAxBranch -> BranchIndex -> CoAxBranch
    forall i e. Ix i => Array i e -> i -> e
    ! BranchIndex
    n

    numBranches :: Branches br -> Int
    numBranches :: forall (br :: BranchFlag). Branches br -> BranchIndex
    numBranches (MkBranches Array BranchIndex CoAxBranch
    arr) = (BranchIndex, BranchIndex) -> BranchIndex
    forall a b. (a, b) -> b
    snd (Array BranchIndex CoAxBranch -> (BranchIndex, BranchIndex)
    forall i e. Array i e -> (i, i)
    bounds Array BranchIndex CoAxBranch
    arr) BranchIndex -> BranchIndex -> BranchIndex
    forall a. Num a => a -> a -> a
    + BranchIndex
    1

    -- | The @[CoAxBranch]@ passed into the mapping function is a list of
    -- all previous branches, reversed
    mapAccumBranches :: ([CoAxBranch] -> CoAxBranch -> CoAxBranch)
                      -> Branches br -> Branches br
    mapAccumBranches :: forall (br :: BranchFlag).
    ([CoAxBranch] -> CoAxBranch -> CoAxBranch)
    -> Branches br -> Branches br
    mapAccumBranches [CoAxBranch] -> CoAxBranch -> CoAxBranch
    f (MkBranches Array BranchIndex CoAxBranch
    arr)
      = Array BranchIndex CoAxBranch -> Branches br
    forall (br :: BranchFlag).
    Array BranchIndex CoAxBranch -> Branches br
    MkBranches ((BranchIndex, BranchIndex)
    -> [CoAxBranch] -> Array BranchIndex CoAxBranch
    forall i e. Ix i => (i, i) -> [e] -> Array i e
    listArray (Array BranchIndex CoAxBranch -> (BranchIndex, BranchIndex)
    forall i e. Array i e -> (i, i)
    bounds Array BranchIndex CoAxBranch
    arr) (([CoAxBranch], [CoAxBranch]) -> [CoAxBranch]
    forall a b. (a, b) -> b
    snd (([CoAxBranch], [CoAxBranch]) -> [CoAxBranch])
    -> ([CoAxBranch], [CoAxBranch]) -> [CoAxBranch]
    forall a b. (a -> b) -> a -> b
    $ ([CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch))
    -> [CoAxBranch] -> [CoAxBranch] -> ([CoAxBranch], [CoAxBranch])
    forall (t :: * -> *) s a b.
    Traversable t =>
    (s -> a -> (s, b)) -> s -> t a -> (s, t b)
    mapAccumL [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
    go [] (Array BranchIndex CoAxBranch -> [CoAxBranch]
    forall i e. Array i e -> [e]
    elems Array BranchIndex CoAxBranch
    arr)))
      where
        go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
        go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
    go [CoAxBranch]
    prev_branches CoAxBranch
    cur_branch = ( CoAxBranch
    cur_branch CoAxBranch -> [CoAxBranch] -> [CoAxBranch]
    forall a. a -> [a] -> [a]
    : [CoAxBranch]
    prev_branches
                                      , [CoAxBranch] -> CoAxBranch -> CoAxBranch
    f [CoAxBranch]
    prev_branches CoAxBranch
    cur_branch )

    {-
    ************************************************************************
    *                                                                      *
                        Coercion axioms
    *                                                                      *
    ************************************************************************

    Note [Storing compatibility]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    During axiom application, we need to be aware of which branches are compatible
    with which others. The full explanation is in Note [Compatibility] in
    GHc.Core.FamInstEnv. (The code is placed there to avoid a dependency from
    GHC.Core.Coercion.Axiom on the unification algorithm.) Although we could
    theoretically compute compatibility on the fly, this is silly, so we store it
    in a CoAxiom.

    Specifically, each branch refers to all other branches with which it is
    incompatible. This list might well be empty, and it will always be for the
    first branch of any axiom.

    CoAxBranches that do not (yet) belong to a CoAxiom should have a panic thunk
    stored in cab_incomps. The incompatibilities are properly a property of the
    axiom as a whole, and they are computed only when the final axiom is built.

    During serialization, the list is converted into a list of the indices
    of the branches.

    Note [CoAxioms are homogeneous]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    All axioms must be *homogeneous*, meaning that the kind of the LHS must
    match the kind of the RHS. In practice, this means:

      Given a CoAxiom { co_ax_tc = ax_tc },
      for every branch CoAxBranch { cab_lhs = lhs, cab_rhs = rhs }:
        typeKind (mkTyConApp ax_tc lhs) `eqType` typeKind rhs

    This is checked in FamInstEnv.mkCoAxBranch.
    -}

    -- | A 'CoAxiom' is a \"coercion constructor\", i.e. a named equality axiom.

    -- If you edit this type, you may need to update the GHC formalism
    -- See Note [GHC Formalism] in GHC.Core.Lint
    data CoAxiom br
      = CoAxiom                   -- Type equality axiom.
        { forall (br :: BranchFlag). CoAxiom br -> Unique
    co_ax_unique   :: Unique        -- Unique identifier
        , forall (br :: BranchFlag). CoAxiom br -> Name
    co_ax_name     :: Name          -- Name for pretty-printing
        , forall (br :: BranchFlag). CoAxiom br -> Role
    co_ax_role     :: Role          -- Role of the axiom's equality
        , forall (br :: BranchFlag). CoAxiom br -> TyCon
    co_ax_tc       :: TyCon         -- The head of the LHS patterns
                                          -- e.g.  the newtype or family tycon
        , forall (br :: BranchFlag). CoAxiom br -> Branches br
    co_ax_branches :: Branches br   -- The branches that form this axiom
        , forall (br :: BranchFlag). CoAxiom br -> Bool
    co_ax_implicit :: Bool          -- True <=> the axiom is "implicit"
                                          -- See Note [Implicit axioms]
             -- INVARIANT: co_ax_implicit == True implies length co_ax_branches == 1.
        }

    -- | A branch of a coercion axiom, which provides the evidence for
    -- unwrapping a newtype or a type-family reduction step using a single equation.
    data CoAxBranch
      = CoAxBranch
        { CoAxBranch -> SrcSpan
    cab_loc      :: SrcSpan
            -- ^ Location of the defining equation
            -- See Note [CoAxiom locations]
        , CoAxBranch -> [TyVar]
    cab_tvs      :: [TyVar]
           -- ^ Bound type variables; not necessarily fresh
           -- See Note [CoAxBranch type variables]
        , CoAxBranch -> [TyVar]
    cab_eta_tvs  :: [TyVar]
           -- ^ Eta-reduced tyvars
           -- cab_tvs and cab_lhs may be eta-reduced; see
           -- Note [Eta reduction for data families]
        , CoAxBranch -> [TyVar]
    cab_cvs      :: [CoVar]
          -- ^ Bound coercion variables
           -- Always empty, for now.
           -- See Note [Constraints in patterns]
           -- in GHC.Tc.TyCl
        , CoAxBranch -> [Role]
    cab_roles    :: [Role]
           -- ^ See Note [CoAxBranch roles]
        , CoAxBranch -> [Type]
    cab_lhs      :: [Type]
           -- ^ Type patterns to match against
        , CoAxBranch -> Type
    cab_rhs      :: Type
           -- ^ Right-hand side of the equality
           -- See Note [CoAxioms are homogeneous]
        , CoAxBranch -> [CoAxBranch]
    cab_incomps  :: [CoAxBranch]
           -- ^ The previous incompatible branches
           -- See Note [Storing compatibility]
        }
      deriving Typeable CoAxBranch
    Typeable CoAxBranch =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> CoAxBranch -> c CoAxBranch)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c CoAxBranch)
    -> (CoAxBranch -> Constr)
    -> (CoAxBranch -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c CoAxBranch))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c CoAxBranch))
    -> ((forall b. Data b => b -> b) -> CoAxBranch -> CoAxBranch)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r)
    -> (forall u. (forall d. Data d => d -> u) -> CoAxBranch -> [u])
    -> (forall u.
        BranchIndex -> (forall d. Data d => d -> u) -> CoAxBranch -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch)
    -> Data CoAxBranch
    CoAxBranch -> Constr
    CoAxBranch -> DataType
    (forall b. Data b => b -> b) -> CoAxBranch -> CoAxBranch
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u.
        BranchIndex -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u.
    BranchIndex -> (forall d. Data d => d -> u) -> CoAxBranch -> u
    forall u. (forall d. Data d => d -> u) -> CoAxBranch -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CoAxBranch
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> CoAxBranch -> c CoAxBranch
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CoAxBranch)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoAxBranch)
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> CoAxBranch -> c CoAxBranch
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> CoAxBranch -> c CoAxBranch
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CoAxBranch
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CoAxBranch
    $ctoConstr :: CoAxBranch -> Constr
    toConstr :: CoAxBranch -> Constr
    $cdataTypeOf :: CoAxBranch -> DataType
    dataTypeOf :: CoAxBranch -> DataType
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CoAxBranch)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CoAxBranch)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoAxBranch)
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoAxBranch)
    $cgmapT :: (forall b. Data b => b -> b) -> CoAxBranch -> CoAxBranch
    gmapT :: (forall b. Data b => b -> b) -> CoAxBranch -> CoAxBranch
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> CoAxBranch -> [u]
    gmapQ :: forall u. (forall d. Data d => d -> u) -> CoAxBranch -> [u]
    $cgmapQi :: forall u.
    BranchIndex -> (forall d. Data d => d -> u) -> CoAxBranch -> u
    gmapQi :: forall u.
    BranchIndex -> (forall d. Data d => d -> u) -> CoAxBranch -> u
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch
    Data.Data

    toBranchedAxiom :: CoAxiom br -> CoAxiom Branched
    toBranchedAxiom :: forall (br :: BranchFlag). CoAxiom br -> CoAxiom Branched
    toBranchedAxiom ax :: CoAxiom br
    ax@(CoAxiom { co_ax_branches :: forall (br :: BranchFlag). CoAxiom br -> Branches br
    co_ax_branches = Branches br
    branches })
      = CoAxiom br
    ax { co_ax_branches = toBranched branches }

    toUnbranchedAxiom :: CoAxiom br -> CoAxiom Unbranched
    toUnbranchedAxiom :: forall (br :: BranchFlag). CoAxiom br -> CoAxiom Unbranched
    toUnbranchedAxiom ax :: CoAxiom br
    ax@(CoAxiom { co_ax_branches :: forall (br :: BranchFlag). CoAxiom br -> Branches br
    co_ax_branches = Branches br
    branches })
      = CoAxiom br
    ax { co_ax_branches = toUnbranched branches }

    coAxiomNumPats :: CoAxiom br -> Int
    coAxiomNumPats :: forall (br :: BranchFlag). CoAxiom br -> BranchIndex
    coAxiomNumPats = [Type] -> BranchIndex
    forall a. [a] -> BranchIndex
    forall (t :: * -> *) a. Foldable t => t a -> BranchIndex
    length ([Type] -> BranchIndex)
    -> (CoAxiom br -> [Type]) -> CoAxiom br -> BranchIndex
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CoAxBranch -> [Type]
    coAxBranchLHS (CoAxBranch -> [Type])
    -> (CoAxiom br -> CoAxBranch) -> CoAxiom br -> [Type]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((CoAxiom br -> BranchIndex -> CoAxBranch)
    -> BranchIndex -> CoAxiom br -> CoAxBranch
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip CoAxiom br -> BranchIndex -> CoAxBranch
    forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> CoAxBranch
    coAxiomNthBranch BranchIndex
    0)

    coAxiomArity :: CoAxiom br -> BranchIndex -> Arity
    coAxiomArity :: forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> BranchIndex
    coAxiomArity CoAxiom br
    ax BranchIndex
    index
      = [TyVar] -> BranchIndex
    forall a. [a] -> BranchIndex
    forall (t :: * -> *) a. Foldable t => t a -> BranchIndex
    length [TyVar]
    tvs BranchIndex -> BranchIndex -> BranchIndex
    forall a. Num a => a -> a -> a
    + [TyVar] -> BranchIndex
    forall a. [a] -> BranchIndex
    forall (t :: * -> *) a. Foldable t => t a -> BranchIndex
    length [TyVar]
    cvs
      where
        CoAxBranch { cab_tvs :: CoAxBranch -> [TyVar]
    cab_tvs = [TyVar]
    tvs, cab_cvs :: CoAxBranch -> [TyVar]
    cab_cvs = [TyVar]
    cvs } = CoAxiom br -> BranchIndex -> CoAxBranch
    forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> CoAxBranch
    coAxiomNthBranch CoAxiom br
    ax BranchIndex
    index
    coAxiomName :: CoAxiom br -> Name
    coAxiomName :: forall (br :: BranchFlag). CoAxiom br -> Name
    coAxiomName = CoAxiom br -> Name
    forall (br :: BranchFlag). CoAxiom br -> Name
    co_ax_name

    coAxiomRole :: CoAxiom br -> Role
    coAxiomRole :: forall (br :: BranchFlag). CoAxiom br -> Role
    coAxiomRole = CoAxiom br -> Role
    forall (br :: BranchFlag). CoAxiom br -> Role
    co_ax_role

    coAxiomBranches :: CoAxiom br -> Branches br
    coAxiomBranches :: forall (br :: BranchFlag). CoAxiom br -> Branches br
    coAxiomBranches = CoAxiom br -> Branches br
    forall (br :: BranchFlag). CoAxiom br -> Branches br
    co_ax_branches

    coAxiomNthBranch :: CoAxiom br -> BranchIndex -> CoAxBranch
    coAxiomNthBranch :: forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> CoAxBranch
    coAxiomNthBranch (CoAxiom { co_ax_branches :: forall (br :: BranchFlag). CoAxiom br -> Branches br
    co_ax_branches = Branches br
    bs }) BranchIndex
    index
      = Branches br -> BranchIndex -> CoAxBranch
    forall (br :: BranchFlag). Branches br -> BranchIndex -> CoAxBranch
    branchesNth Branches br
    bs BranchIndex
    index

    coAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch
    coAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch
    coAxiomSingleBranch (CoAxiom { co_ax_branches :: forall (br :: BranchFlag). CoAxiom br -> Branches br
    co_ax_branches = MkBranches Array BranchIndex CoAxBranch
    arr })
      = Array BranchIndex CoAxBranch
    arr Array BranchIndex CoAxBranch -> BranchIndex -> CoAxBranch
    forall i e. Ix i => Array i e -> i -> e
    ! BranchIndex
    0

    coAxiomSingleBranch_maybe :: CoAxiom br -> Maybe CoAxBranch
    coAxiomSingleBranch_maybe :: forall (br :: BranchFlag). CoAxiom br -> Maybe CoAxBranch
    coAxiomSingleBranch_maybe (CoAxiom { co_ax_branches :: forall (br :: BranchFlag). CoAxiom br -> Branches br
    co_ax_branches = MkBranches Array BranchIndex CoAxBranch
    arr })
      | (BranchIndex, BranchIndex) -> BranchIndex
    forall a b. (a, b) -> b
    snd (Array BranchIndex CoAxBranch -> (BranchIndex, BranchIndex)
    forall i e. Array i e -> (i, i)
    bounds Array BranchIndex CoAxBranch
    arr) BranchIndex -> BranchIndex -> Bool
    forall a. Eq a => a -> a -> Bool
    == BranchIndex
    0
      = CoAxBranch -> Maybe CoAxBranch
    forall a. a -> Maybe a
    Just (CoAxBranch -> Maybe CoAxBranch) -> CoAxBranch -> Maybe CoAxBranch
    forall a b. (a -> b) -> a -> b
    $ Array BranchIndex CoAxBranch
    arr Array BranchIndex CoAxBranch -> BranchIndex -> CoAxBranch
    forall i e. Ix i => Array i e -> i -> e
    ! BranchIndex
    0
      | Bool
    otherwise
      = Maybe CoAxBranch
    forall a. Maybe a
    Nothing

    coAxiomTyCon :: CoAxiom br -> TyCon
    coAxiomTyCon :: forall (br :: BranchFlag). CoAxiom br -> TyCon
    coAxiomTyCon = CoAxiom br -> TyCon
    forall (br :: BranchFlag). CoAxiom br -> TyCon
    co_ax_tc

    coAxBranchTyVars :: CoAxBranch -> [TyVar]
    coAxBranchTyVars :: CoAxBranch -> [TyVar]
    coAxBranchTyVars = CoAxBranch -> [TyVar]
    cab_tvs

    coAxBranchCoVars :: CoAxBranch -> [CoVar]
    coAxBranchCoVars :: CoAxBranch -> [TyVar]
    coAxBranchCoVars = CoAxBranch -> [TyVar]
    cab_cvs

    coAxBranchLHS :: CoAxBranch -> [Type]
    coAxBranchLHS :: CoAxBranch -> [Type]
    coAxBranchLHS = CoAxBranch -> [Type]
    cab_lhs

    coAxBranchRHS :: CoAxBranch -> Type
    coAxBranchRHS :: CoAxBranch -> Type
    coAxBranchRHS = CoAxBranch -> Type
    cab_rhs

    coAxBranchRoles :: CoAxBranch -> [Role]
    coAxBranchRoles :: CoAxBranch -> [Role]
    coAxBranchRoles = CoAxBranch -> [Role]
    cab_roles

    coAxBranchSpan :: CoAxBranch -> SrcSpan
    coAxBranchSpan :: CoAxBranch -> SrcSpan
    coAxBranchSpan = CoAxBranch -> SrcSpan
    cab_loc

    isImplicitCoAxiom :: CoAxiom br -> Bool
    isImplicitCoAxiom :: forall (br :: BranchFlag). CoAxiom br -> Bool
    isImplicitCoAxiom = CoAxiom br -> Bool
    forall (br :: BranchFlag). CoAxiom br -> Bool
    co_ax_implicit

    coAxBranchIncomps :: CoAxBranch -> [CoAxBranch]
    coAxBranchIncomps :: CoAxBranch -> [CoAxBranch]
    coAxBranchIncomps = CoAxBranch -> [CoAxBranch]
    cab_incomps

    -- See Note [Compatibility] in GHC.Core.FamInstEnv
    placeHolderIncomps :: [CoAxBranch]
    placeHolderIncomps :: [CoAxBranch]
    placeHolderIncomps = String -> [CoAxBranch]
    forall a. HasCallStack => String -> a
    panic String
    "placeHolderIncomps"

    {-
    Note [CoAxBranch type variables]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    In the case of a CoAxBranch of an associated type-family instance,
    we use the *same* type variables in cab_tvs (where possible) as the
    enclosing class or instance.  Consider

      instance C Int [z] where
         type F Int [z] = ...   -- Second param must be [z]

    In the CoAxBranch in the instance decl (F Int [z]) we use the
    same 'z', so that it's easy to check that that type is the same
    as that in the instance header.

    However, I believe that the cab_tvs of any CoAxBranch are distinct
    from the cab_tvs of other CoAxBranches in the same CoAxiom.  This is
    important when checking for compatiblity and apartness; e.g. see
    GHC.Core.FamInstEnv.compatibleBranches.  (The story seems a bit wobbly
    here, but it seems to work.)

    Note [CoAxBranch roles]
    ~~~~~~~~~~~~~~~~~~~~~~~
    Consider this code:

      newtype Age = MkAge Int
      newtype Wrap a = MkWrap a

      convert :: Wrap Age -> Int
      convert (MkWrap (MkAge i)) = i

    We want this to compile to:

      NTCo:Wrap :: forall a. Wrap a ~R a
      NTCo:Age  :: Age ~R Int
      convert = \x -> x |> (NTCo:Wrap[0] NTCo:Age[0])

    But, note that NTCo:Age is at role R. Thus, we need to be able to pass
    coercions at role R into axioms. However, we don't *always* want to be able to
    do this, as it would be disastrous with type families. The solution is to
    annotate the arguments to the axiom with roles, much like we annotate tycon
    tyvars. Where do these roles get set? Newtype axioms inherit their roles from
    the newtype tycon; family axioms are all at role N.

    Note [CoAxiom locations]
    ~~~~~~~~~~~~~~~~~~~~~~~~
    The source location of a CoAxiom is stored in two places in the
    datatype tree.
      * The first is in the location info buried in the Name of the
        CoAxiom. This span includes all of the branches of a branched
        CoAxiom.
      * The second is in the cab_loc fields of the CoAxBranches.

    In the case of a single branch, we can extract the source location of
    the branch from the name of the CoAxiom. In other cases, we need an
    explicit SrcSpan to correctly store the location of the equation
    giving rise to the FamInstBranch.

    Note [Implicit axioms]
    ~~~~~~~~~~~~~~~~~~~~~~
    See also Note [Implicit TyThings] in GHC.Types.TyThing
    * A CoAxiom arising from data/type family instances is not "implicit".
      That is, it has its own IfaceAxiom declaration in an interface file

    * The CoAxiom arising from a newtype declaration *is* "implicit".
      That is, it does not have its own IfaceAxiom declaration in an
      interface file; instead the CoAxiom is generated by type-checking
      the newtype declaration

    Note [Eta reduction for data families]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Consider this
       data family T a b :: *
       newtype instance T Int a = MkT (IO a) deriving( Monad )
    We'd like this to work.

    From the 'newtype instance' you might think we'd get:
       newtype TInt a = MkT (IO a)
       axiom ax1 a :: T Int a ~ TInt a   -- The newtype-instance part
       axiom ax2 a :: TInt a ~ IO a      -- The newtype part

    But now what can we do?  We have this problem
       Given:   d  :: Monad IO
       Wanted:  d' :: Monad (T Int) = d |> ????
    What coercion can we use for the ???

    Solution: eta-reduce both axioms, thus:
       axiom ax1 :: T Int ~ TInt
       axiom ax2 :: TInt ~ IO
    Now
       d' = d |> Monad (sym (ax2 ; ax1))

    ----- Bottom line ------

    For a CoAxBranch for a data family instance with representation
    TyCon rep_tc:

      - cab_tvs (of its CoAxiom) may be shorter
        than tyConTyVars of rep_tc.

      - cab_lhs may be shorter than tyConArity of the family tycon
           i.e. LHS is unsaturated

      - cab_rhs will be (rep_tc cab_tvs)
           i.e. RHS is un-saturated

      - This eta reduction happens for data instances as well
        as newtype instances. Here we want to eta-reduce the data family axiom.

      - This eta-reduction is done in GHC.Tc.TyCl.Instance.tcDataFamInstDecl.

    But for a /type/ family
      - cab_lhs has the exact arity of the family tycon

    There are certain situations (e.g., pretty-printing) where it is necessary to
    deal with eta-expanded data family instances. For these situations, the
    cab_eta_tvs field records the stuff that has been eta-reduced away.
    So if we have
        axiom forall a b. F [a->b] = D b a
    and cab_eta_tvs is [p,q], then the original user-written definition
    looked like
        axiom forall a b p q. F [a->b] p q = D b a p q
    (See #9692, #14179, and #15845 for examples of what can go wrong if
    we don't eta-expand when showing things to the user.)

    See also:

    * Note [Newtype eta] in GHC.Core.TyCon.  This is notionally separate
      and deals with the axiom connecting a newtype with its representation
      type; but it too is eta-reduced.
    * Note [Implementing eta reduction for data families] in "GHC.Tc.TyCl.Instance". This
      describes the implementation details of this eta reduction happen.
    * Note [RoughMap and rm_empty] for how this complicates the RoughMap implementation slightly.
    -}

    {- *********************************************************************
    *                                                                      *
                  Instances, especially pretty-printing
    *                                                                      *
    ********************************************************************* -}

    instance Eq (CoAxiom br) where
        CoAxiom br
    a == :: CoAxiom br -> CoAxiom br -> Bool
    == CoAxiom br
    b = CoAxiom br -> Unique
    forall a. Uniquable a => a -> Unique
    getUnique CoAxiom br
    a Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == CoAxiom br -> Unique
    forall a. Uniquable a => a -> Unique
    getUnique CoAxiom br
    b
        CoAxiom br
    a /= :: CoAxiom br -> CoAxiom br -> Bool
    /= CoAxiom br
    b = CoAxiom br -> Unique
    forall a. Uniquable a => a -> Unique
    getUnique CoAxiom br
    a Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    /= CoAxiom br -> Unique
    forall a. Uniquable a => a -> Unique
    getUnique CoAxiom br
    b

    instance Uniquable (CoAxiom br) where
        getUnique :: CoAxiom br -> Unique
    getUnique = CoAxiom br -> Unique
    forall (br :: BranchFlag). CoAxiom br -> Unique
    co_ax_unique

    instance NamedThing (CoAxiom br) where
        getName :: CoAxiom br -> Name
    getName = CoAxiom br -> Name
    forall (br :: BranchFlag). CoAxiom br -> Name
    co_ax_name

    instance Typeable br => Data.Data (CoAxiom br) where
        -- don't traverse?
        toConstr :: CoAxiom br -> Constr
    toConstr CoAxiom br
    _   = String -> Constr
    abstractConstr String
    "CoAxiom"
        gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (CoAxiom br)
    gunfold forall b r. Data b => c (b -> r) -> c r
    _ forall r. r -> c r
    _  = String -> Constr -> c (CoAxiom br)
    forall a. HasCallStack => String -> a
    error String
    "gunfold"
        dataTypeOf :: CoAxiom br -> DataType
    dataTypeOf CoAxiom br
    _ = String -> DataType
    mkNoRepType String
    "CoAxiom"

    instance Outputable (CoAxiom br) where
      -- You may want GHC.Core.Coercion.pprCoAxiom instead
      ppr :: CoAxiom br -> SDoc
    ppr = Name -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (Name -> SDoc) -> (CoAxiom br -> Name) -> CoAxiom br -> SDoc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CoAxiom br -> Name
    forall a. NamedThing a => a -> Name
    getName

    instance Outputable CoAxBranch where
      -- This instance doesn't know the name of the type family
      -- If possible, use GHC.Core.Coercion.pprCoAxBranch instead
      ppr :: CoAxBranch -> SDoc
    ppr (CoAxBranch { cab_tvs :: CoAxBranch -> [TyVar]
    cab_tvs = [TyVar]
    tvs, cab_cvs :: CoAxBranch -> [TyVar]
    cab_cvs = [TyVar]
    cvs
                      , cab_lhs :: CoAxBranch -> [Type]
    cab_lhs = [Type]
    lhs_tys, cab_rhs :: CoAxBranch -> Type
    cab_rhs = Type
    rhs, cab_incomps :: CoAxBranch -> [CoAxBranch]
    cab_incomps = [CoAxBranch]
    incomps })
        = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "CoAxBranch" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc
    braces SDoc
    payload
        where
          payload :: SDoc
    payload = SDoc -> BranchIndex -> SDoc -> SDoc
    hang (String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "forall" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> (TyVar -> SDoc) -> [TyVar] -> SDoc
    forall a. (a -> SDoc) -> [a] -> SDoc
    pprWithCommas TyVar -> SDoc
    pprTyVar ([TyVar]
    tvs [TyVar] -> [TyVar] -> [TyVar]
    forall a. [a] -> [a] -> [a]
    ++ [TyVar]
    cvs) SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> SDoc
    forall doc. IsLine doc => doc
    dot)
                       BranchIndex
    2 ([SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat [ String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "<tycon>" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> [SDoc] -> SDoc
    forall doc. IsLine doc => [doc] -> doc
    sep ((Type -> SDoc) -> [Type] -> [SDoc]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> SDoc
    pprType [Type]
    lhs_tys)
                               , BranchIndex -> SDoc -> SDoc
    nest BranchIndex
    2 (String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "=" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Type
    rhs)
                               , Bool -> SDoc -> SDoc
    forall doc. IsOutput doc => Bool -> doc -> doc
    ppUnless ([CoAxBranch] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [CoAxBranch]
    incomps) (SDoc -> SDoc) -> SDoc -> SDoc
    forall a b. (a -> b) -> a -> b
    $
                                 String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "incomps:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> [SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat ((CoAxBranch -> SDoc) -> [CoAxBranch] -> [SDoc]
    forall a b. (a -> b) -> [a] -> [b]
    map CoAxBranch -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [CoAxBranch]
    incomps) ])

    {-
    ************************************************************************
    *                                                                      *
                        Roles
    *                                                                      *
    ************************************************************************

    Roles are defined here to avoid circular dependencies.
    -}

    -- These names are slurped into the parser code. Changing these strings
    -- will change the **surface syntax** that GHC accepts! If you want to
    -- change only the pretty-printing, do some replumbing. See
    -- mkRoleAnnotDecl in GHC.Parser.PostProcess
    fsFromRole :: Role -> FastString
    fsFromRole :: Role -> FastString
    fsFromRole Role
    Nominal          = String -> FastString
    fsLit String
    "nominal"
    fsFromRole Role
    Representational = String -> FastString
    fsLit String
    "representational"
    fsFromRole Role
    Phantom          = String -> FastString
    fsLit String
    "phantom"

    instance Outputable Role where
      ppr :: Role -> SDoc
    ppr = FastString -> SDoc
    forall doc. IsLine doc => FastString -> doc
    ftext (FastString -> SDoc) -> (Role -> FastString) -> Role -> SDoc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Role -> FastString
    fsFromRole

    instance Binary Role where
      put_ :: WriteBinHandle -> Role -> IO ()
    put_ WriteBinHandle
    bh Role
    Nominal          = WriteBinHandle -> Word8 -> IO ()
    putByte WriteBinHandle
    bh Word8
    1
      put_ WriteBinHandle
    bh Role
    Representational = WriteBinHandle -> Word8 -> IO ()
    putByte WriteBinHandle
    bh Word8
    2
      put_ WriteBinHandle
    bh Role
    Phantom          = WriteBinHandle -> Word8 -> IO ()
    putByte WriteBinHandle
    bh Word8
    3

      get :: ReadBinHandle -> IO Role
    get ReadBinHandle
    bh = do tag <- ReadBinHandle -> IO Word8
    getByte ReadBinHandle
    bh
                  case tag of Word8
    1 -> Role -> IO Role
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Role
    Nominal
                              Word8
    2 -> Role -> IO Role
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Role
    Representational
                              Word8
    3 -> Role -> IO Role
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Role
    Phantom
                              Word8
    _ -> String -> IO Role
    forall a. HasCallStack => String -> a
    panic (String
    "get Role " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Word8 -> String
    forall a. Show a => a -> String
    show Word8
    tag)

    {-
    ************************************************************************
    *                                                                      *
                        CoAxiomRule
                  Rules for building Evidence
    *                                                                      *
    ************************************************************************

    Note [CoAxiomRule]
    ~~~~~~~~~~~~~~~~~~
    A CoAxiomRule is a built-in axiom, one that we assume to be true:
    CoAxiomRules come in four flavours:

    * BuiltInFamRew: provides evidence for, say
          (ax1)    3+4 ----> 7
          (ax2)    s+0 ----> s
      The evidence looks like
          AxiomCo ax1 [3,4] :: 3+4 ~ 7
          AxiomCo ax2 [s]   :: s+0 ~ s
      The arguments in the AxiomCo are the /instantiating types/, or
      more generally coercions (see Note [Coercion axioms applied to coercions]
      in GHC.Core.TyCo.Rep).

    * BuiltInFamInj: provides evidence for the injectivity of type families
      For example
          (ax3)   g1: a+b ~ 0        --->  a~0
          (ax4)   g2: a+b ~ 0        --->  b~0
          (ax5)   g3: a+b1 ~ a~b2    --->  b1~b2
      The argument to the AxiomCo is the full coercion (always just one).
      So then:
          AxiomCo ax3 [g1] :: a ~ 0
          AxiomCo ax4 [g2] :: b ~ 0
          AxiomCo ax5 [g3] :: b1 ~ b2

    * BranchedAxiom: used for closed type families
          type family F a where
            F Int  = Bool
            F Bool = Char
            F a    = a -> Int
      We get one (CoAxiom Branched) for the entire family; when used in an
      AxiomCo we pair it with the BranchIndex to say which branch to pick.

    * UnbranchedAxiom: used for several purposes;
        - Newtypes
        - Data family instances
        - Open type family instances

    Note [Avoiding allocating lots of CoAxiomRules]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    CoAxiomRule is a sum type of four alternatives, which is very nice. But
    there is a danger of allocating lots of (BuiltInFamRew bif) objects, every
    time we (say) need a type-family rewrite.

    To avoid this allocation, we cache the appropraite CoAxiomRule inside each
       BuiltInFamRewrite, BuiltInFamInjectivity
    making a little circular data structure.  See the `bifrw_axr` field of
    BuiltInFamRewrite, and similarly the others.

    It's simple to do this, and saves a percent or two of allocation in programs
    that do a lot of type-family work.
    -}

    -- | CoAxiomRule describes a built-in axiom, one that we assume to be true
    -- See Note [CoAxiomRule]
    data CoAxiomRule
      = BuiltInFamRew  BuiltInFamRewrite                   -- Built-in type-family rewrites
                                                           --    e.g.  3+5 ~ 7

      | BuiltInFamInj  BuiltInFamInjectivity               -- Built-in type-family deductions
                                                           --    e.g.  a+b~0 ==>  a~0
                                                           -- Always unary

      | BranchedAxiom      (CoAxiom Branched) BranchIndex  -- Closed type family

      | UnbranchedAxiom    (CoAxiom Unbranched)            -- Open type family instance,
                                                           --    data family instances
                                                           --    and newtypes

    instance Eq CoAxiomRule where
      (BuiltInFamRew  BuiltInFamRewrite
    bif1)  == :: CoAxiomRule -> CoAxiomRule -> Bool
    == (BuiltInFamRew  BuiltInFamRewrite
    bif2)  = BuiltInFamRewrite -> FastString
    bifrw_name  BuiltInFamRewrite
    bif1 FastString -> FastString -> Bool
    forall a. Eq a => a -> a -> Bool
    == BuiltInFamRewrite -> FastString
    bifrw_name BuiltInFamRewrite
    bif2
      (BuiltInFamInj BuiltInFamInjectivity
    bif1)   == (BuiltInFamInj BuiltInFamInjectivity
    bif2)   = BuiltInFamInjectivity -> FastString
    bifinj_name BuiltInFamInjectivity
    bif1 FastString -> FastString -> Bool
    forall a. Eq a => a -> a -> Bool
    == BuiltInFamInjectivity -> FastString
    bifinj_name BuiltInFamInjectivity
    bif2
      (UnbranchedAxiom CoAxiom Unbranched
    ax1)  == (UnbranchedAxiom CoAxiom Unbranched
    ax2)  = CoAxiom Unbranched -> Unique
    forall a. Uniquable a => a -> Unique
    getUnique CoAxiom Unbranched
    ax1 Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == CoAxiom Unbranched -> Unique
    forall a. Uniquable a => a -> Unique
    getUnique CoAxiom Unbranched
    ax2
      (BranchedAxiom CoAxiom Branched
    ax1 BranchIndex
    i1) == (BranchedAxiom CoAxiom Branched
    ax2 BranchIndex
    i2) = CoAxiom Branched -> Unique
    forall a. Uniquable a => a -> Unique
    getUnique CoAxiom Branched
    ax1 Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == CoAxiom Branched -> Unique
    forall a. Uniquable a => a -> Unique
    getUnique CoAxiom Branched
    ax2 Bool -> Bool -> Bool
    && BranchIndex
    i1 BranchIndex -> BranchIndex -> Bool
    forall a. Eq a => a -> a -> Bool
    == BranchIndex
    i2
      CoAxiomRule
    _ == CoAxiomRule
    _ = Bool
    False

    coAxiomRuleRole :: CoAxiomRule -> Role
    coAxiomRuleRole :: CoAxiomRule -> Role
    coAxiomRuleRole (BuiltInFamRew  {})  = Role
    Nominal
    coAxiomRuleRole (BuiltInFamInj {})   = Role
    Nominal
    coAxiomRuleRole (UnbranchedAxiom CoAxiom Unbranched
    ax) = CoAxiom Unbranched -> Role
    forall (br :: BranchFlag). CoAxiom br -> Role
    coAxiomRole CoAxiom Unbranched
    ax
    coAxiomRuleRole (BranchedAxiom CoAxiom Branched
    ax BranchIndex
    _) = CoAxiom Branched -> Role
    forall (br :: BranchFlag). CoAxiom br -> Role
    coAxiomRole CoAxiom Branched
    ax

    coAxiomRuleArgRoles :: CoAxiomRule -> [Role]
    coAxiomRuleArgRoles :: CoAxiomRule -> [Role]
    coAxiomRuleArgRoles (BuiltInFamRew  BuiltInFamRewrite
    bif) = BranchIndex -> Role -> [Role]
    forall a. BranchIndex -> a -> [a]
    replicate (BuiltInFamRewrite -> BranchIndex
    bifrw_arity BuiltInFamRewrite
    bif) Role
    Nominal
    coAxiomRuleArgRoles (BuiltInFamInj {})   = [Role
    Nominal]
    coAxiomRuleArgRoles (UnbranchedAxiom CoAxiom Unbranched
    ax) = CoAxBranch -> [Role]
    coAxBranchRoles (CoAxiom Unbranched -> CoAxBranch
    coAxiomSingleBranch CoAxiom Unbranched
    ax)
    coAxiomRuleArgRoles (BranchedAxiom CoAxiom Branched
    ax BranchIndex
    i) = CoAxBranch -> [Role]
    coAxBranchRoles (CoAxiom Branched -> BranchIndex -> CoAxBranch
    forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> CoAxBranch
    coAxiomNthBranch CoAxiom Branched
    ax BranchIndex
    i)

    coAxiomRuleBranch_maybe :: CoAxiomRule -> Maybe (TyCon, Role, CoAxBranch)
    coAxiomRuleBranch_maybe :: CoAxiomRule -> Maybe (TyCon, Role, CoAxBranch)
    coAxiomRuleBranch_maybe (UnbranchedAxiom CoAxiom Unbranched
    ax) = (TyCon, Role, CoAxBranch) -> Maybe (TyCon, Role, CoAxBranch)
    forall a. a -> Maybe a
    Just (CoAxiom Unbranched -> TyCon
    forall (br :: BranchFlag). CoAxiom br -> TyCon
    co_ax_tc CoAxiom Unbranched
    ax, CoAxiom Unbranched -> Role
    forall (br :: BranchFlag). CoAxiom br -> Role
    co_ax_role CoAxiom Unbranched
    ax, CoAxiom Unbranched -> CoAxBranch
    coAxiomSingleBranch CoAxiom Unbranched
    ax)
    coAxiomRuleBranch_maybe (BranchedAxiom CoAxiom Branched
    ax BranchIndex
    i) = (TyCon, Role, CoAxBranch) -> Maybe (TyCon, Role, CoAxBranch)
    forall a. a -> Maybe a
    Just (CoAxiom Branched -> TyCon
    forall (br :: BranchFlag). CoAxiom br -> TyCon
    co_ax_tc CoAxiom Branched
    ax, CoAxiom Branched -> Role
    forall (br :: BranchFlag). CoAxiom br -> Role
    co_ax_role CoAxiom Branched
    ax, CoAxiom Branched -> BranchIndex -> CoAxBranch
    forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> CoAxBranch
    coAxiomNthBranch CoAxiom Branched
    ax BranchIndex
    i)
    coAxiomRuleBranch_maybe CoAxiomRule
    _                    = Maybe (TyCon, Role, CoAxBranch)
    forall a. Maybe a
    Nothing

    isNewtypeAxiomRule_maybe :: CoAxiomRule -> Maybe (TyCon, CoAxBranch)
    isNewtypeAxiomRule_maybe :: CoAxiomRule -> Maybe (TyCon, CoAxBranch)
    isNewtypeAxiomRule_maybe (UnbranchedAxiom CoAxiom Unbranched
    ax)
      | let tc :: TyCon
    tc = CoAxiom Unbranched -> TyCon
    forall (br :: BranchFlag). CoAxiom br -> TyCon
    coAxiomTyCon CoAxiom Unbranched
    ax, TyCon -> Bool
    isNewTyCon TyCon
    tc = (TyCon, CoAxBranch) -> Maybe (TyCon, CoAxBranch)
    forall a. a -> Maybe a
    Just (TyCon
    tc, CoAxiom Unbranched -> CoAxBranch
    coAxiomSingleBranch CoAxiom Unbranched
    ax)
    isNewtypeAxiomRule_maybe CoAxiomRule
    _                  = Maybe (TyCon, CoAxBranch)
    forall a. Maybe a
    Nothing

    instance Data.Data CoAxiomRule where
      -- don't traverse?
      toConstr :: CoAxiomRule -> Constr
    toConstr CoAxiomRule
    _   = String -> Constr
    abstractConstr String
    "CoAxiomRule"
      gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CoAxiomRule
    gunfold forall b r. Data b => c (b -> r) -> c r
    _ forall r. r -> c r
    _  = String -> Constr -> c CoAxiomRule
    forall a. HasCallStack => String -> a
    error String
    "gunfold"
      dataTypeOf :: CoAxiomRule -> DataType
    dataTypeOf CoAxiomRule
    _ = String -> DataType
    mkNoRepType String
    "CoAxiomRule"

    instance Outputable CoAxiomRule where
      ppr :: CoAxiomRule -> SDoc
    ppr (BuiltInFamRew  BuiltInFamRewrite
    bif) = FastString -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (BuiltInFamRewrite -> FastString
    bifrw_name BuiltInFamRewrite
    bif)
      ppr (BuiltInFamInj BuiltInFamInjectivity
    bif)  = FastString -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (BuiltInFamInjectivity -> FastString
    bifinj_name BuiltInFamInjectivity
    bif)
      ppr (UnbranchedAxiom CoAxiom Unbranched
    ax) = Name -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (CoAxiom Unbranched -> Name
    forall (br :: BranchFlag). CoAxiom br -> Name
    coAxiomName CoAxiom Unbranched
    ax)
      ppr (BranchedAxiom CoAxiom Branched
    ax BranchIndex
    i) = Name -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (CoAxiom Branched -> Name
    forall (br :: BranchFlag). CoAxiom br -> Name
    coAxiomName CoAxiom Branched
    ax) SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc
    brackets (BranchIndex -> SDoc
    forall doc. IsLine doc => BranchIndex -> doc
    int BranchIndex
    i)

    {- *********************************************************************
    *                                                                      *
                        Built-in families
    *                                                                      *
    ********************************************************************* -}

    -- | A more explicit representation for `t1 ~ t2`.
    type TypeEqn = Pair Type

    -- Type checking of built-in families
    data BuiltInSynFamily = BuiltInSynFamily
      { BuiltInSynFamily -> [BuiltInFamRewrite]
    sfMatchFam :: [BuiltInFamRewrite]
      , BuiltInSynFamily -> [BuiltInFamInjectivity]
    sfInteract :: [BuiltInFamInjectivity]
        -- If given these type arguments and RHS, returns the equalities that
        -- are guaranteed to hold.  That is, if
        --     (ar, Pair s1 s2)  is an element of  (sfInteract tys ty)
        -- then  AxiomRule ar [co :: F tys ~ ty]  ::  s1~s2
      }

    data BuiltInFamInjectivity  -- Argument and result role are always Nominal
      = BIF_Interact
          { BuiltInFamInjectivity -> FastString
    bifinj_name :: FastString
          , BuiltInFamInjectivity -> CoAxiomRule
    bifinj_axr  :: CoAxiomRule -- Cached copy of (BuiltInFamINj this-bif)
                                       -- See Note [Avoiding allocating lots of CoAxiomRules]

          , BuiltInFamInjectivity -> TypeEqn -> Maybe TypeEqn
    bifinj_proves :: TypeEqn -> Maybe TypeEqn
                -- ^ Always unary: just one TypeEqn argument
                -- Returns @Nothing@ when it doesn't like the supplied argument.
                -- When this happens in a coercion that means that the coercion is
                -- ill-formed, and Core Lint checks for that.
          }

    data BuiltInFamRewrite  -- Argument roles and result role are always Nominal
      = BIF_Rewrite
          { BuiltInFamRewrite -> FastString
    bifrw_name   :: FastString
          , BuiltInFamRewrite -> CoAxiomRule
    bifrw_axr    :: CoAxiomRule -- Cached copy of (BuiltInFamRew this-bif)
                                        -- See Note [Avoiding allocating lots of CoAxiomRules]

          , BuiltInFamRewrite -> TyCon
    bifrw_fam_tc :: TyCon       -- Needed for tyConsOfType

          , BuiltInFamRewrite -> BranchIndex
    bifrw_arity  :: Arity       -- Number of type arguments needed
                                        -- to instantiate this axiom

          , BuiltInFamRewrite -> [Type] -> Maybe ([Type], Type)
    bifrw_match :: [Type] -> Maybe ([Type], Type)
               -- coaxrMatch: does this reduce on the given arguments?
               -- If it does, returns (types to instantiate the rule at, rhs type)
               -- That is: mkAxiomCo ax (zipWith mkReflCo coAxiomRuleArgRoles ts)
               --              :: F tys ~N rhs,

          , BuiltInFamRewrite -> [TypeEqn] -> Maybe TypeEqn
    bifrw_proves :: [TypeEqn] -> Maybe TypeEqn }
               -- length(inst_tys) = bifrw_arity

          -- INVARIANT: bifrw_match and bifrw_proves are related as follows:
          -- If    Just (inst_tys, res_ty) = bifrw_match ax arg_tys
          -- then  * length arg_tys = tyConArity fam_tc
          --       * length inst_tys = bifrw_arity
           --      * bifrw_proves (map (return @Pair) inst_tys) = Just (return @Pair res_ty)

    -- Provides default implementations that do nothing.
    trivialBuiltInFamily :: BuiltInSynFamily
    trivialBuiltInFamily :: BuiltInSynFamily
    trivialBuiltInFamily = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
    sfMatchFam = [], sfInteract :: [BuiltInFamInjectivity]
    sfInteract = [] }