Commit 2a3702d8 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Comments and tiny refactor

Related to Ryan's upcoming patch for Trac #14933
parent 0693b0b0
......@@ -257,6 +257,10 @@ data IfaceCoercion
| IfaceForAllCo IfaceTvBndr IfaceCoercion IfaceCoercion
| IfaceCoVarCo IfLclName
| IfaceAxiomInstCo IfExtName BranchIndex [IfaceCoercion]
| IfaceAxiomRuleCo IfLclName [IfaceCoercion]
-- There are only a fixed number of CoAxiomRules, so it suffices
-- to use an IfaceLclName to distinguish them.
-- See Note [Adding built-in type families] in TcTypeNats
| IfaceUnivCo IfaceUnivCoProv Role IfaceType IfaceType
| IfaceSymCo IfaceCoercion
| IfaceTransCo IfaceCoercion IfaceCoercion
......@@ -266,7 +270,6 @@ data IfaceCoercion
| IfaceCoherenceCo IfaceCoercion IfaceCoercion
| IfaceKindCo IfaceCoercion
| IfaceSubCo IfaceCoercion
| IfaceAxiomRuleCo IfLclName [IfaceCoercion]
| IfaceFreeCoVar CoVar -- See Note [Free tyvars in IfaceType]
| IfaceHoleCo CoVar -- ^ See Note [Holes in IfaceCoercion]
......
......@@ -1359,7 +1359,7 @@ tcIfaceCo = go
<*> go c2
go (IfaceKindCo c) = KindCo <$> go c
go (IfaceSubCo c) = SubCo <$> go c
go (IfaceAxiomRuleCo ax cos) = AxiomRuleCo <$> go_axiom_rule ax
go (IfaceAxiomRuleCo ax cos) = AxiomRuleCo <$> tcIfaceCoAxiomRule ax
<*> mapM go cos
go (IfaceFreeCoVar c) = pprPanic "tcIfaceCo:IfaceFreeCoVar" (ppr c)
go (IfaceHoleCo c) = pprPanic "tcIfaceCo:IfaceHoleCo" (ppr c)
......@@ -1367,12 +1367,6 @@ tcIfaceCo = go
go_var :: FastString -> IfL CoVar
go_var = tcIfaceLclId
go_axiom_rule :: FastString -> IfL CoAxiomRule
go_axiom_rule n =
case Map.lookup n typeNatCoAxiomRules of
Just ax -> return ax
_ -> pprPanic "go_axiom_rule" (ppr n)
tcIfaceUnivCoProv :: IfaceUnivCoProv -> IfL UnivCoProvenance
tcIfaceUnivCoProv IfaceUnsafeCoerceProv = return UnsafeCoerceProv
tcIfaceUnivCoProv (IfacePhantomProv kco) = PhantomProv <$> tcIfaceCo kco
......@@ -1808,6 +1802,16 @@ tcIfaceCoAxiom :: Name -> IfL (CoAxiom Branched)
tcIfaceCoAxiom name = do { thing <- tcIfaceImplicit name
; return (tyThingCoAxiom thing) }
tcIfaceCoAxiomRule :: IfLclName -> IfL CoAxiomRule
-- Unlike CoAxioms, which arise form user 'type instance' declarations,
-- there are a fixed set of CoAxiomRules,
-- currently enumerated in typeNatCoAxiomRules
tcIfaceCoAxiomRule n
= case Map.lookup n typeNatCoAxiomRules of
Just ax -> return ax
_ -> pprPanic "go_axiom_rule" (ppr n)
tcIfaceDataCon :: Name -> IfL DataCon
tcIfaceDataCon name = do { thing <- tcIfaceGlobal name
; case thing of
......
{-# LANGUAGE LambdaCase #-}
{- Note [Type-level natural numbers]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
See the Wiki page:
https://ghc.haskell.org/trac/ghc/wiki/TypeNats
and Note [Adding built-in type families]
-}
module TcTypeNats
( typeNatTyCons
, typeNatCoAxiomRules
......
......@@ -814,16 +814,17 @@ data Coercion
-- any left over, we use AppCo.
-- See [Coercion axioms applied to coercions]
| AxiomRuleCo CoAxiomRule [Coercion]
-- AxiomRuleCo is very like AxiomInstCo, but for a CoAxiomRule
-- The number coercions should match exactly the expectations
-- of the CoAxiomRule (i.e., the rule is fully saturated).
| UnivCo UnivCoProvenance Role Type Type
-- :: _ -> "e" -> _ -> _ -> e
| SymCo Coercion -- :: e -> e
| TransCo Coercion Coercion -- :: e -> e -> e
-- The number coercions should match exactly the expectations
-- of the CoAxiomRule (i.e., the rule is fully saturated).
| AxiomRuleCo CoAxiomRule [Coercion]
| NthCo Int Coercion -- Zero-indexed; decomposes (T t0 ... tn)
-- :: _ -> e -> ?? (inverse of TyConAppCo, see Note [TyConAppCo roles])
-- Using NthCo on a ForAllCo gives an N coercion always
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment