{-# 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 = [] }