-- (c) The University of Glasgow 2012 {-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, GADTs, KindSignatures, ScopedTypeVariables, StandaloneDeriving, RoleAnnotations #-} -- | Module for coercion axioms, used to represent type family instances -- and newtypes module CoAxiom ( 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(..), TypeEqn, BuiltInSynFamily(..), trivialBuiltInFamily ) where import GhcPrelude import {-# SOURCE #-} TyCoRep ( Type, pprType ) import {-# SOURCE #-} TyCon ( TyCon ) import Outputable import FastString import Name import Unique import Var import Util import Binary import Pair import BasicTypes import Data.Typeable ( Typeable ) import SrcLoc import qualified Data.Data as Data import Data.Array import Data.List ( mapAccumL ) #include "HsVersions.h" {- 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 AxiomInstCo 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 -- AxiomInstCo 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 FamInstEnv.hs. 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 * * ************************************************************************ -} type BranchIndex = Int -- The index of the branch in the list of branches -- Counting from zero -- 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 { Branches br -> Array BranchIndex CoAxBranch unMkBranches :: Array BranchIndex CoAxBranch } type role Branches nominal manyBranches :: [CoAxBranch] -> Branches Branched manyBranches :: [CoAxBranch] -> Branches Branched manyBranches brs :: [CoAxBranch] brs = ASSERT( snd bnds >= fst 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 = (0, [CoAxBranch] -> BranchIndex forall (t :: * -> *) a. Foldable t => t a -> BranchIndex length [CoAxBranch] brs BranchIndex -> BranchIndex -> BranchIndex forall a. Num a => a -> a -> a - 1) unbranched :: CoAxBranch -> Branches Unbranched unbranched :: CoAxBranch -> Branches Unbranched unbranched br :: 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 (0, 0) [CoAxBranch br]) toBranched :: Branches br -> Branches Branched toBranched :: 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 :: Branches br -> Branches Unbranched toUnbranched (MkBranches arr :: Array BranchIndex CoAxBranch arr) = ASSERT( bounds arr == (0,0) ) Array BranchIndex CoAxBranch -> Branches Unbranched forall (br :: BranchFlag). Array BranchIndex CoAxBranch -> Branches br MkBranches Array BranchIndex CoAxBranch arr fromBranches :: Branches br -> [CoAxBranch] fromBranches :: 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 :: Branches br -> BranchIndex -> CoAxBranch branchesNth (MkBranches arr :: Array BranchIndex CoAxBranch arr) n :: 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 :: Branches br -> BranchIndex numBranches (MkBranches arr :: 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 + 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 :: ([CoAxBranch] -> CoAxBranch -> CoAxBranch) -> Branches br -> Branches br mapAccumBranches f :: [CoAxBranch] -> CoAxBranch -> CoAxBranch f (MkBranches arr :: 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 :: * -> *) a b c. Traversable t => (a -> b -> (a, c)) -> a -> t b -> (a, t c) 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 prev_branches :: [CoAxBranch] prev_branches cur_branch :: 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 FamInstEnv. (The code is placed there to avoid a dependency from CoAxiom 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. -} -- | 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 coreSyn/CoreLint.hs data CoAxiom br = CoAxiom -- Type equality axiom. { CoAxiom br -> Unique co_ax_unique :: Unique -- Unique identifier , CoAxiom br -> Name co_ax_name :: Name -- Name for pretty-printing , CoAxiom br -> Role co_ax_role :: Role -- Role of the axiom's equality , CoAxiom br -> TyCon co_ax_tc :: TyCon -- The head of the LHS patterns -- e.g. the newtype or family tycon , CoAxiom br -> Branches br co_ax_branches :: Branches br -- The branches that form this axiom , 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. } 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 , CoAxBranch -> [TyVar] cab_eta_tvs :: [TyVar] -- Eta-reduced tyvars -- See Note [CoAxBranch type variables] -- cab_tvs and cab_lhs may be eta-reduded; 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 TcTyClsDecls , CoAxBranch -> [Role] cab_roles :: [Role] -- See Note [CoAxBranch roles] , CoAxBranch -> [Type] cab_lhs :: [Type] -- Type patterns to match against -- See Note [CoAxiom saturation] , CoAxBranch -> Type cab_rhs :: Type -- Right-hand side of the equality , CoAxBranch -> [CoAxBranch] cab_incomps :: [CoAxBranch] -- The previous incompatible branches -- See Note [Storing compatibility] } deriving Typeable CoAxBranch DataType Constr 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 -> DataType CoAxBranch -> Constr (forall b. Data b => b -> b) -> CoAxBranch -> CoAxBranch (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoAxBranch -> c CoAxBranch (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c 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) $cCoAxBranch :: Constr $tCoAxBranch :: DataType gmapMo :: (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 gmapMp :: (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 gmapM :: (forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch gmapQi :: BranchIndex -> (forall d. Data d => d -> u) -> CoAxBranch -> u $cgmapQi :: forall u. BranchIndex -> (forall d. Data d => d -> u) -> CoAxBranch -> u gmapQ :: (forall d. Data d => d -> u) -> CoAxBranch -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> CoAxBranch -> [u] gmapQr :: (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 gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r gmapT :: (forall b. Data b => b -> b) -> CoAxBranch -> CoAxBranch $cgmapT :: (forall b. Data b => b -> b) -> CoAxBranch -> CoAxBranch dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoAxBranch) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoAxBranch) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c CoAxBranch) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CoAxBranch) dataTypeOf :: CoAxBranch -> DataType $cdataTypeOf :: CoAxBranch -> DataType toConstr :: CoAxBranch -> Constr $ctoConstr :: CoAxBranch -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoAxBranch $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoAxBranch gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoAxBranch -> c CoAxBranch $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoAxBranch -> c CoAxBranch $cp1Data :: Typeable CoAxBranch Data.Data toBranchedAxiom :: CoAxiom br -> CoAxiom Branched toBranchedAxiom :: CoAxiom br -> CoAxiom Branched toBranchedAxiom (CoAxiom unique :: Unique unique name :: Name name role :: Role role tc :: TyCon tc branches :: Branches br branches implicit :: Bool implicit) = Unique -> Name -> Role -> TyCon -> Branches Branched -> Bool -> CoAxiom Branched forall (br :: BranchFlag). Unique -> Name -> Role -> TyCon -> Branches br -> Bool -> CoAxiom br CoAxiom Unique unique Name name Role role TyCon tc (Branches br -> Branches Branched forall (br :: BranchFlag). Branches br -> Branches Branched toBranched Branches br branches) Bool implicit toUnbranchedAxiom :: CoAxiom br -> CoAxiom Unbranched toUnbranchedAxiom :: CoAxiom br -> CoAxiom Unbranched toUnbranchedAxiom (CoAxiom unique :: Unique unique name :: Name name role :: Role role tc :: TyCon tc branches :: Branches br branches implicit :: Bool implicit) = Unique -> Name -> Role -> TyCon -> Branches Unbranched -> Bool -> CoAxiom Unbranched forall (br :: BranchFlag). Unique -> Name -> Role -> TyCon -> Branches br -> Bool -> CoAxiom br CoAxiom Unique unique Name name Role role TyCon tc (Branches br -> Branches Unbranched forall (br :: BranchFlag). Branches br -> Branches Unbranched toUnbranched Branches br branches) Bool implicit coAxiomNumPats :: CoAxiom br -> Int coAxiomNumPats :: CoAxiom br -> BranchIndex coAxiomNumPats = [Type] -> 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 0) coAxiomNthBranch :: CoAxiom br -> BranchIndex -> CoAxBranch coAxiomNthBranch :: CoAxiom br -> BranchIndex -> CoAxBranch coAxiomNthBranch (CoAxiom { co_ax_branches :: forall (br :: BranchFlag). CoAxiom br -> Branches br co_ax_branches = Branches br bs }) index :: BranchIndex index = Branches br -> BranchIndex -> CoAxBranch forall (br :: BranchFlag). Branches br -> BranchIndex -> CoAxBranch branchesNth Branches br bs BranchIndex index coAxiomArity :: CoAxiom br -> BranchIndex -> Arity coAxiomArity :: CoAxiom br -> BranchIndex -> BranchIndex coAxiomArity ax :: CoAxiom br ax index :: BranchIndex index = [TyVar] -> 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 (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 :: CoAxiom br -> Name coAxiomName = CoAxiom br -> Name forall (br :: BranchFlag). CoAxiom br -> Name co_ax_name coAxiomRole :: CoAxiom br -> Role coAxiomRole :: CoAxiom br -> Role coAxiomRole = CoAxiom br -> Role forall (br :: BranchFlag). CoAxiom br -> Role co_ax_role coAxiomBranches :: CoAxiom br -> Branches br coAxiomBranches :: CoAxiom br -> Branches br coAxiomBranches = CoAxiom br -> Branches br forall (br :: BranchFlag). CoAxiom br -> Branches br co_ax_branches coAxiomSingleBranch_maybe :: CoAxiom br -> Maybe CoAxBranch coAxiomSingleBranch_maybe :: CoAxiom br -> Maybe CoAxBranch coAxiomSingleBranch_maybe (CoAxiom { co_ax_branches :: forall (br :: BranchFlag). CoAxiom br -> Branches br co_ax_branches = MkBranches arr :: 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 == 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 ! 0 | Bool otherwise = Maybe CoAxBranch forall a. Maybe a Nothing coAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch coAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch coAxiomSingleBranch (CoAxiom { co_ax_branches :: forall (br :: BranchFlag). CoAxiom br -> Branches br co_ax_branches = MkBranches arr :: Array BranchIndex CoAxBranch arr }) = Array BranchIndex CoAxBranch arr Array BranchIndex CoAxBranch -> BranchIndex -> CoAxBranch forall i e. Ix i => Array i e -> i -> e ! 0 coAxiomTyCon :: CoAxiom br -> TyCon coAxiomTyCon :: 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 :: 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 checking] in FamInstEnv placeHolderIncomps :: [CoAxBranch] placeHolderIncomps :: [CoAxBranch] placeHolderIncomps = String -> [CoAxBranch] forall a. String -> a panic "placeHolderIncomps" {- Note [CoAxiom saturation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * When co Note [CoAxBranch type variables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In the case of a CoAxBranch of an associated type-family instance, we use the *same* type variables (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. So, unlike FamInsts, there is no expectation that the cab_tvs are fresh wrt each other, or any other CoAxBranch. 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 HscTypes * 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 TcInstDcls.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 TyCon. This is notionally separate and deals with the axiom connecting a newtype with its representation type; but it too is eta-reduced.) -} instance Eq (CoAxiom br) where a :: CoAxiom br a == :: CoAxiom br -> CoAxiom br -> Bool == b :: 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 a :: CoAxiom br a /= :: CoAxiom br -> CoAxiom br -> Bool /= b :: 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 Outputable (CoAxiom br) where 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 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 _ = String -> Constr abstractConstr "CoAxiom" gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (CoAxiom br) gunfold _ _ = String -> Constr -> c (CoAxiom br) forall a. HasCallStack => String -> a error "gunfold" dataTypeOf :: CoAxiom br -> DataType dataTypeOf _ = String -> DataType mkNoRepType "CoAxiom" instance Outputable CoAxBranch where ppr :: CoAxBranch -> SDoc ppr (CoAxBranch { cab_loc :: CoAxBranch -> SrcSpan cab_loc = SrcSpan loc , cab_lhs :: CoAxBranch -> [Type] cab_lhs = [Type] lhs , cab_rhs :: CoAxBranch -> Type cab_rhs = Type rhs }) = String -> SDoc text "CoAxBranch" SDoc -> SDoc -> SDoc <+> SDoc -> SDoc parens (SrcSpan -> SDoc forall a. Outputable a => a -> SDoc ppr SrcSpan loc) SDoc -> SDoc -> SDoc <> SDoc colon SDoc -> SDoc -> SDoc <+> SDoc -> SDoc brackets ([SDoc] -> SDoc fsep (SDoc -> [SDoc] -> [SDoc] punctuate SDoc comma ((Type -> SDoc) -> [Type] -> [SDoc] forall a b. (a -> b) -> [a] -> [b] map Type -> SDoc pprType [Type] lhs))) SDoc -> SDoc -> SDoc <+> String -> SDoc text "=>" SDoc -> SDoc -> SDoc <+> Type -> SDoc pprType Type rhs {- ************************************************************************ * * Roles * * ************************************************************************ Roles are defined here to avoid circular dependencies. -} -- See Note [Roles] in Coercion -- defined here to avoid cyclic dependency with Coercion -- -- Order of constructors matters: the Ord instance coincides with the *super*typing -- relation on roles. data Role = Nominal | Representational | Phantom deriving (Role -> Role -> Bool (Role -> Role -> Bool) -> (Role -> Role -> Bool) -> Eq Role forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Role -> Role -> Bool $c/= :: Role -> Role -> Bool == :: Role -> Role -> Bool $c== :: Role -> Role -> Bool Eq, Eq Role Eq Role => (Role -> Role -> Ordering) -> (Role -> Role -> Bool) -> (Role -> Role -> Bool) -> (Role -> Role -> Bool) -> (Role -> Role -> Bool) -> (Role -> Role -> Role) -> (Role -> Role -> Role) -> Ord Role Role -> Role -> Bool Role -> Role -> Ordering Role -> Role -> Role forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: Role -> Role -> Role $cmin :: Role -> Role -> Role max :: Role -> Role -> Role $cmax :: Role -> Role -> Role >= :: Role -> Role -> Bool $c>= :: Role -> Role -> Bool > :: Role -> Role -> Bool $c> :: Role -> Role -> Bool <= :: Role -> Role -> Bool $c<= :: Role -> Role -> Bool < :: Role -> Role -> Bool $c< :: Role -> Role -> Bool compare :: Role -> Role -> Ordering $ccompare :: Role -> Role -> Ordering $cp1Ord :: Eq Role Ord, Typeable Role DataType Constr Typeable Role => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Role -> c Role) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Role) -> (Role -> Constr) -> (Role -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Role)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role)) -> ((forall b. Data b => b -> b) -> Role -> Role) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r) -> (forall u. (forall d. Data d => d -> u) -> Role -> [u]) -> (forall u. BranchIndex -> (forall d. Data d => d -> u) -> Role -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Role -> m Role) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role) -> Data Role Role -> DataType Role -> Constr (forall b. Data b => b -> b) -> Role -> Role (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Role -> c Role (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Role 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) -> Role -> u forall u. (forall d. Data d => d -> u) -> Role -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Role -> m Role forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Role forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Role -> c Role forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Role) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role) $cPhantom :: Constr $cRepresentational :: Constr $cNominal :: Constr $tRole :: DataType gmapMo :: (forall d. Data d => d -> m d) -> Role -> m Role $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role gmapMp :: (forall d. Data d => d -> m d) -> Role -> m Role $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role gmapM :: (forall d. Data d => d -> m d) -> Role -> m Role $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Role -> m Role gmapQi :: BranchIndex -> (forall d. Data d => d -> u) -> Role -> u $cgmapQi :: forall u. BranchIndex -> (forall d. Data d => d -> u) -> Role -> u gmapQ :: (forall d. Data d => d -> u) -> Role -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Role -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r gmapT :: (forall b. Data b => b -> b) -> Role -> Role $cgmapT :: (forall b. Data b => b -> b) -> Role -> Role dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Role) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Role) dataTypeOf :: Role -> DataType $cdataTypeOf :: Role -> DataType toConstr :: Role -> Constr $ctoConstr :: Role -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Role $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Role gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Role -> c Role $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Role -> c Role $cp1Data :: Typeable Role Data.Data) -- 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 RdrHsSyn fsFromRole :: Role -> FastString fsFromRole :: Role -> FastString fsFromRole Nominal = String -> FastString fsLit "nominal" fsFromRole Representational = String -> FastString fsLit "representational" fsFromRole Phantom = String -> FastString fsLit "phantom" instance Outputable Role where ppr :: Role -> SDoc ppr = FastString -> SDoc 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_ :: BinHandle -> Role -> IO () put_ bh :: BinHandle bh Nominal = BinHandle -> Word8 -> IO () putByte BinHandle bh 1 put_ bh :: BinHandle bh Representational = BinHandle -> Word8 -> IO () putByte BinHandle bh 2 put_ bh :: BinHandle bh Phantom = BinHandle -> Word8 -> IO () putByte BinHandle bh 3 get :: BinHandle -> IO Role get bh :: BinHandle bh = do Word8 tag <- BinHandle -> IO Word8 getByte BinHandle bh case Word8 tag of 1 -> Role -> IO Role forall (m :: * -> *) a. Monad m => a -> m a return Role Nominal 2 -> Role -> IO Role forall (m :: * -> *) a. Monad m => a -> m a return Role Representational 3 -> Role -> IO Role forall (m :: * -> *) a. Monad m => a -> m a return Role Phantom _ -> String -> IO Role forall a. String -> a panic ("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 * * ************************************************************************ Conditional axioms. The general idea is that a `CoAxiomRule` looks like this: forall as. (r1 ~ r2, s1 ~ s2) => t1 ~ t2 My intention is to reuse these for both (~) and (~#). The short-term plan is to use this datatype to represent the type-nat axioms. In the longer run, it may be good to unify this and `CoAxiom`, as `CoAxiom` is the special case when there are no assumptions. -} -- | A more explicit representation for `t1 ~ t2`. type TypeEqn = Pair Type -- | For now, we work only with nominal equality. data CoAxiomRule = CoAxiomRule { CoAxiomRule -> FastString coaxrName :: FastString , CoAxiomRule -> [Role] coaxrAsmpRoles :: [Role] -- roles of parameter equations , CoAxiomRule -> Role coaxrRole :: Role -- role of resulting equation , CoAxiomRule -> [TypeEqn] -> Maybe TypeEqn coaxrProves :: [TypeEqn] -> Maybe TypeEqn -- ^ coaxrProves returns @Nothing@ when it doesn't like -- the supplied arguments. When this happens in a coercion -- that means that the coercion is ill-formed, and Core Lint -- checks for that. } instance Data.Data CoAxiomRule where -- don't traverse? toConstr :: CoAxiomRule -> Constr toConstr _ = String -> Constr abstractConstr "CoAxiomRule" gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoAxiomRule gunfold _ _ = String -> Constr -> c CoAxiomRule forall a. HasCallStack => String -> a error "gunfold" dataTypeOf :: CoAxiomRule -> DataType dataTypeOf _ = String -> DataType mkNoRepType "CoAxiomRule" instance Uniquable CoAxiomRule where getUnique :: CoAxiomRule -> Unique getUnique = FastString -> Unique forall a. Uniquable a => a -> Unique getUnique (FastString -> Unique) -> (CoAxiomRule -> FastString) -> CoAxiomRule -> Unique forall b c a. (b -> c) -> (a -> b) -> a -> c . CoAxiomRule -> FastString coaxrName instance Eq CoAxiomRule where x :: CoAxiomRule x == :: CoAxiomRule -> CoAxiomRule -> Bool == y :: CoAxiomRule y = CoAxiomRule -> FastString coaxrName CoAxiomRule x FastString -> FastString -> Bool forall a. Eq a => a -> a -> Bool == CoAxiomRule -> FastString coaxrName CoAxiomRule y instance Ord CoAxiomRule where compare :: CoAxiomRule -> CoAxiomRule -> Ordering compare x :: CoAxiomRule x y :: CoAxiomRule y = FastString -> FastString -> Ordering forall a. Ord a => a -> a -> Ordering compare (CoAxiomRule -> FastString coaxrName CoAxiomRule x) (CoAxiomRule -> FastString coaxrName CoAxiomRule y) instance Outputable CoAxiomRule where ppr :: CoAxiomRule -> SDoc ppr = FastString -> SDoc forall a. Outputable a => a -> SDoc ppr (FastString -> SDoc) -> (CoAxiomRule -> FastString) -> CoAxiomRule -> SDoc forall b c a. (b -> c) -> (a -> b) -> a -> c . CoAxiomRule -> FastString coaxrName -- Type checking of built-in families data BuiltInSynFamily = BuiltInSynFamily { BuiltInSynFamily -> [Type] -> Maybe (CoAxiomRule, [Type], Type) sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type) , BuiltInSynFamily -> [Type] -> Type -> [TypeEqn] sfInteractTop :: [Type] -> Type -> [TypeEqn] , BuiltInSynFamily -> [Type] -> Type -> [Type] -> Type -> [TypeEqn] sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn] } -- Provides default implementations that do nothing. trivialBuiltInFamily :: BuiltInSynFamily trivialBuiltInFamily :: BuiltInSynFamily trivialBuiltInFamily = BuiltInSynFamily :: ([Type] -> Maybe (CoAxiomRule, [Type], Type)) -> ([Type] -> Type -> [TypeEqn]) -> ([Type] -> Type -> [Type] -> Type -> [TypeEqn]) -> BuiltInSynFamily BuiltInSynFamily { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type) sfMatchFam = \_ -> Maybe (CoAxiomRule, [Type], Type) forall a. Maybe a Nothing , sfInteractTop :: [Type] -> Type -> [TypeEqn] sfInteractTop = \_ _ -> [] , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn] sfInteractInert = \_ _ _ _ -> [] }