core-spec: Modify file paths according to new module hierarchy

This patch updates file paths according to new module hierarchy [1]:

  * GHC/Core.hs                <= coreSyn/CoreSyn.hs
  * GHC/Core/Coercion.hs       <= types/Coercion.hs
  * GHC/Core/Coercion/Axiom.hs <= types/CoAxiom.hs
  * GHC/Core/Coercion/Opt.hs   <= types/OptCoercion.hs
  * GHC/Core/DataCon.hs        <= basicTypes/DataCon.hs
  * GHC/Core/FamInstEnv.hs     <= types/FamInstEnv.hs
  * GHC/Core/Lint.hs           <= coreSyn/CoreLint.hs
  * GHC/Core/Subst.hs          <= coreSyn/CoreSubst.hs
  * GHC/Core/TyCo/Rep.hs       <= types/TyCoRep.hs
  * GHC/Core/TyCon.hs          <= types/TyCon.hs
  * GHC/Core/Type.hs           <= types/Type.hs
  * GHC/Core/Unify.hs          <= types/Unify.hs
  * GHC/Types/Literal.hs       <= basicTypes/Literal.hs
  * GHC/Types/Var.hs           <= basicTypes/Var.hs

[1]: https://gitlab.haskell.org/ghc/ghc/-/wikis/Make-GHC-codebase-more-modular

[skip ci]

5 files changed, 68 insertions, 68 deletions

diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 9ce8584f9a..6aff07c499 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -12,7 +12,7 @@
 defns
 CoreLint :: '' ::=
 
-defn |- prog program ::  :: lintCoreBindings :: 'Prog_' {{ com Program typing, \coderef{coreSyn/CoreLint.hs}{lintCoreBindings} }}
+defn |- prog program ::  :: lintCoreBindings :: 'Prog_' {{ com Program typing, \coderef{GHC/Core/Lint.hs}{lintCoreBindings} }}
   {{ tex \labeledjudge{prog} [[program]] }}
 by
 
@@ -22,7 +22,7 @@ no_duplicates </ bindingi // i />
 --------------------- :: CoreBindings
 |-prog </ bindingi // i />
 
-defn G |- bind binding ::  :: lint_bind :: 'Binding_' {{ com Binding typing, \coderef{coreSyn/CoreLint.hs}{lint\_bind} }}
+defn G |- bind binding ::  :: lint_bind :: 'Binding_' {{ com Binding typing, \coderef{GHC/Core/Lint.hs}{lint\_bind} }}
   {{ tex [[G]] \labeledjudge{bind} [[binding]] }}
 by
 
@@ -34,7 +34,7 @@ G |-bind n = e
 ---------------------- :: Rec
 G |-bind rec </ ni = ei // i />
 
-defn G  |- sbind n <- e ::  :: lintSingleBinding :: 'SBinding_' {{ com Single binding typing, \coderef{coreSyn/CoreLint.hs}{lintSingleBinding} }}
+defn G  |- sbind n <- e ::  :: lintSingleBinding :: 'SBinding_' {{ com Single binding typing, \coderef{GHC/Core/Lint.hs}{lintSingleBinding} }}
   {{ tex [[G]] \labeledjudge{sbind} [[n]] [[<-]] [[e]] }}
 by
 
@@ -45,7 +45,7 @@ G |-name z_t ok
 ----------------- :: SingleBinding
 G |-sbind z_t <- e
 
-defn G ; D |-sjbind l vars <- e : t ::  :: lintSingleBinding_joins :: 'SJBinding_' {{ com Single join binding typing, \coderef{coreSyn/CoreLint.hs}{lintSingleBinding} }}
+defn G ; D |-sjbind l vars <- e : t ::  :: lintSingleBinding_joins :: 'SJBinding_' {{ com Single join binding typing, \coderef{GHC/Core/Lint.hs}{lintSingleBinding} }}
   {{ tex [[G]];[[D]] \labeledjudge{sjbind} [[l]] \, [[vars]] [[<-]] [[e]] : [[t]] }}
 by
 
@@ -60,7 +60,7 @@ split_I s = </ sj // j /> t
 G; D |-sjbind p/I_s </ nj // j /> <- e : t
 
 defn G ; D  |- tm e : t ::  :: lintCoreExpr :: 'Tm_'
-  {{ com Expression typing, \coderef{coreSyn/CoreLint.hs}{lintCoreExpr} }}
+  {{ com Expression typing, \coderef{GHC/Core/Lint.hs}{lintCoreExpr} }}
   {{ tex [[G]]; [[D]] \labeledjudge{tm} [[e]] : [[t]] }}
 by
 
@@ -171,7 +171,7 @@ G |-co g : t1 k1~Rep k2 t2
 G; D |-tm g : (~Rep#) k1 k2 t1 t2
 
 defn G  |- name n ok ::  :: lintSingleBinding_lintBinder :: 'Name_'
-  {{ com Name consistency check, \coderef{coreSyn/CoreLint.hs}{lintSingleBinding\#lintBinder} }}
+  {{ com Name consistency check, \coderef{GHC/Core/Lint.hs}{lintSingleBinding\#lintBinder} }}
   {{ tex [[G]] \labeledjudge{n} [[n]] [[ok]] }}
 by
 
@@ -184,7 +184,7 @@ G |-name x_t ok
 G |-name alpha_k ok
 
 defn G |- label l ok ::  :: lintSingleBinding_lintBinder_join :: 'Label_'
-  {{ com Label consistency check, \coderef{coreSyn/CoreLint.hs}{lintSingleBinding\#lintBinder} }}
+  {{ com Label consistency check, \coderef{GHC/Core/Lint.hs}{lintSingleBinding\#lintBinder} }}
   {{ tex [[G]] \labeledjudge{label} [[l]] [[ok]] }}
 by
 
@@ -197,7 +197,7 @@ k' = * \/ k' = #
 G |-label p / I _ t ok
 
 defn G |- bnd n ok ::  :: lintBinder :: 'Binding_'
-  {{ com Binding consistency, \coderef{coreSyn/CoreLint.hs}{lintBinder} }}
+  {{ com Binding consistency, \coderef{GHC/Core/Lint.hs}{lintBinder} }}
   {{ tex [[G]] \labeledjudge{bnd} [[n]] [[ok]] }}
 by
 
@@ -211,7 +211,7 @@ G |-ki k ok
 G |-bnd alpha_k ok
 
 defn G  |- co g : t1 k1 ~ R k2 t2 ::  :: lintCoercion :: 'Co_'
-  {{ com Coercion typing, \coderef{coreSyn/CoreLint.hs}{lintCoercion} }}
+  {{ com Coercion typing, \coderef{GHC/Core/Lint.hs}{lintCoercion} }}
   {{ tex [[G]] \labeledjudge{co} [[g]] : [[t1]] \mathop{ {}^{[[k1]]} {\sim}_{[[R]]}^{[[k2]]} } [[t2]] }}
 by
 
@@ -375,7 +375,7 @@ G |-ty t'2 : k0'
 G |-co mu </ ti // i /> $ </ gj // j /> : t'1 k0 ~R' k0' t'2
 
 defn G |- axk [ namesroles |-> gs ] ~> ( subst1 , subst2 ) ::  :: check_ki :: 'AxiomKind_'
-  {{ com Axiom argument kinding, \coderef{coreSyn/CoreLint.hs}{lintCoercion\#check\_ki} }}
+  {{ com Axiom argument kinding, \coderef{GHC/Core/Lint.hs}{lintCoercion\#check\_ki} }}
   {{ tex [[G]] \labeledjudge{axk} [ [[namesroles]] [[|->]] [[gs]] ] [[~>]] ([[subst1]], [[subst2]]) }}
 by
 
@@ -451,7 +451,7 @@ O |- t |> g : R
 O |- g : Ph
 
 defn R1 <= R2 ::  :: ltRole :: 'Rlt_'
-  {{ com Sub-role relation, \coderef{types/Coercion.hs}{ltRole} }}
+  {{ com Sub-role relation, \coderef{GHC/Core/Coercion.hs}{ltRole} }}
   {{ tex [[R1]] \leq [[R2]] }}
 by
 
@@ -465,7 +465,7 @@ R <= Ph
 R <= R
 
 defn G |- ki k ok ::  :: lintKind :: 'K_'
-  {{ com Kind validity, \coderef{coreSyn/CoreLint.hs}{lintKind} }}
+  {{ com Kind validity, \coderef{GHC/Core/Lint.hs}{lintKind} }}
   {{ tex [[G]] \labeledjudge{k} [[k]] [[ok]] }}
 by
 
@@ -478,7 +478,7 @@ G |-ty k : #
 G |-ki k ok
 
 defn G |- ty t : k ::  :: lintType :: 'Ty_'
-  {{ com Kinding, \coderef{coreSyn/CoreLint.hs}{lintType} }}
+  {{ com Kinding, \coderef{GHC/Core/Lint.hs}{lintType} }}
   {{ tex [[G]] \labeledjudge{ty} [[t]] : [[k]] }}
 by
 
@@ -535,7 +535,7 @@ G |-co g : t1 k1 ~Rep k2 t2
 G |-ty g : (~Rep#) k1 k2 t1 t2
 
 defn G |- subst n |-> t ok ::  :: lintTyKind :: 'Subst_'
-  {{ com Substitution consistency, \coderef{coreSyn/CoreLint.hs}{lintTyKind} }}
+  {{ com Substitution consistency, \coderef{GHC/Core/Lint.hs}{lintTyKind} }}
   {{ tex [[G]] \labeledjudge{subst} [[n]] [[|->]] [[t]] [[ok]] }}
 by
 
@@ -544,7 +544,7 @@ G |-ty t : k
 G |-subst z_k |-> t ok
 
 defn G ; D ; s |- altern alt : t ::  :: lintCoreAlt :: 'Alt_'
-  {{ com Case alternative consistency, \coderef{coreSyn/CoreLint.hs}{lintCoreAlt} }}
+  {{ com Case alternative consistency, \coderef{GHC/Core/Lint.hs}{lintCoreAlt} }}
   {{ tex [[G]];[[D]];[[s]] \labeledjudge{alt} [[alt]] : [[t]] }}
 by
 
@@ -569,7 +569,7 @@ G'; D |-tm e : t
 G; D; T </ sj // j /> |-altern K </ ni // i /> -> e : t
 
 defn t' = t { </ si // , // i /> } ::  :: applyTys :: 'ApplyTys_'
-  {{ com Telescope substitution, \coderef{types/Type.hs}{applyTys} }}
+  {{ com Telescope substitution, \coderef{GHC/Core/Type.hs}{applyTys} }}
 by
 
 --------------------- :: Empty
@@ -581,7 +581,7 @@ t'' = t'[n |-> s]
 t'' = (forall n. t) { s, </ si // i /> }
 
 defn G |- altbnd vars : t1 ~> t2 ::  :: lintAltBinders :: 'AltBinders_'
-  {{ com Case alternative binding consistency, \coderef{coreSyn/CoreLint.hs}{lintAltBinders} }}
+  {{ com Case alternative binding consistency, \coderef{GHC/Core/Lint.hs}{lintAltBinders} }}
   {{ tex [[G]] \labeledjudge{altbnd} [[vars]] : [[t1]] [[~>]] [[t2]] }}
 by
 
@@ -602,7 +602,7 @@ G |-altbnd </ ni // i /> : t2 ~> s
 G |-altbnd x_t1, </ ni // i /> : (t1 -> t2) ~> s
 
 defn G |- arrow k1 -> k2 : k ::  :: lintArrow :: 'Arrow_'
-  {{ com Arrow kinding, \coderef{coreSyn/CoreLint.hs}{lintArrow} }}
+  {{ com Arrow kinding, \coderef{GHC/Core/Lint.hs}{lintArrow} }}
   {{ tex [[G]] \labeledjudge{\rightarrow} [[k1]] [[->]] [[k2]] : [[k]] }}
 by
 
@@ -612,7 +612,7 @@ k2 = TYPE s
 G |-arrow k1 -> k2 : *
 
 defn G |- app kinded_types : k1 ~> k2 ::  :: lint_app :: 'App_'
-  {{ com Type application kinding, \coderef{coreSyn/CoreLint.hs}{lint\_app} }}
+  {{ com Type application kinding, \coderef{GHC/Core/Lint.hs}{lint\_app} }}
   {{ tex [[G]] \labeledjudge{app} [[kinded_types]] : [[k1]] [[~>]] [[k2]] }}
 by
 
@@ -628,7 +628,7 @@ G |-app </ (ti : ki) // i /> : k2[z_k1 |-> t] ~> k'
 G |-app (t : k1), </ (ti : ki) // i /> : (forall z_k1. k2) ~> k'
 
 defn no_conflict ( C , </ sj // j /> , ind1 , ind2 ) ::  :: check_no_conflict :: 'NoConflict_'
-  {{ com \parbox{5in}{Branched axiom conflict checking, \coderef{types/OptCoercion.hs}{checkAxInstCo} \\ and \coderef{types/FamInstEnv.hs}{compatibleBranches} } }}
+  {{ com \parbox{5in}{Branched axiom conflict checking, \coderef{GHC/Core/Coercion/Opt.hs}{checkAxInstCo} \\ and \coderef{GHC/Core/FamInstEnv.hs}{compatibleBranches} } }}
 by
 
 ------------------------------------------------ :: NoBranch
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index c22eb51183..0b9893c3a9 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -34,19 +34,19 @@ indexvar i, j, kk {{ tex k }}, aa {{ tex a }}, bb {{ tex b }}, cc {{ tex c }} ::
 grammar
 
 lit {{ tex \textsf{lit} }} :: 'Literal_' ::=
-  {{ com Literals, \coderef{basicTypes/Literal.hs}{Literal} }}
+  {{ com Literals, \coderef{GHC/Types/Literal.hs}{Literal} }}
 
 z :: 'Name_' ::= {{ com Term or type name }}
   | alpha           ::   :: Type    {{ com Type-level name }}
   | x               ::   :: Term    {{ com Term-level name }}
 
-n, m, aname {{ tex \alpha }}, xname {{ tex x }} :: 'Var_' ::= {{ com Variable names, \coderef{basicTypes/Var.hs}{Var} }}
+n, m, aname {{ tex \alpha }}, xname {{ tex x }} :: 'Var_' ::= {{ com Variable names, \coderef{GHC/Types/Var.hs}{Var} }}
   | z _ t           ::   :: IdOrTyVar   {{ com Name, labeled with type/kind }}
     {{ tex {[[z]]}^{[[t]]} }}
   | z $             :: M :: NoSupScript {{ com Name without an explicit type/kind }}
   | K               :: M :: DataCon     {{ com Data constructor }}
 
-l :: 'Label_' ::= {{ com Labels for join points, also \coderef{basicTypes/Var.hs}{Var} }}
+l :: 'Label_' ::= {{ com Labels for join points, also \coderef{GHC/Types/Var.hs}{Var} }}
   | p / I _ t     ::   :: Label   {{ com Label with join arity and type }}
     {{ tex  {[[p]]}_{[[I]]}^{[[t]]} }}
 
@@ -64,7 +64,7 @@ labels :: 'Labels_' ::= {{ com List of labels }}
   | </ li // , // i />       ::   :: List
   | empty                    :: M :: empty
 
-e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.hs}{Expr} }}
+e, u :: 'Expr_' ::= {{ com Expressions, \coderef{GHC/Core.hs}{Expr} }}
   | n                                            ::   :: Var  {{ com \ctor{Var}: Variable }}
   | lit                                          ::   :: Lit  {{ com \ctor{Lit}: Literal }}
   | e1 e2                                        ::   :: App  {{ com \ctor{App}: Application }}
@@ -85,31 +85,31 @@ e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.hs}{Expr} }}
   | \\ e                                         :: M :: Newline
     {{ tex \qquad \\ \multicolumn{1}{r}{[[e]]} }}
 
-binding :: 'Bind_' ::= {{ com Let-bindings, \coderef{coreSyn/CoreSyn.hs}{Bind} }}
+binding :: 'Bind_' ::= {{ com Let-bindings, \coderef{GHC/Core.hs}{Bind} }}
   | n = e                         ::   :: NonRec  {{ com \ctor{NonRec}: Non-recursive binding }}
   | rec </ ni = ei // ;; // i /> ::   :: Rec     {{ com \ctor{Rec}: Recursive binding }}
 
-jbinding :: 'JoinBind_' ::= {{ com Join bindings, also \coderef{coreSyn/CoreSyn.hs}{Bind} }}
+jbinding :: 'JoinBind_' ::= {{ com Join bindings, also \coderef{GHC/Core.hs}{Bind} }}
   | l </ ni // i /> = e     ::   :: NonRec {{ com \ctor{NonRec}: Non-recursive binding }}
   | rec </ li </ nij // j /> = ei // i /> :: :: Rec {{ com \ctor{Rec}: Recursive binding }}
 
-alt :: 'Alt_' ::= {{ com Case alternative, \coderef{coreSyn/CoreSyn.hs}{Alt} }}
+alt :: 'Alt_' ::= {{ com Case alternative, \coderef{GHC/Core.hs}{Alt} }}
   | Kp </ ni // i /> -> e    ::   :: Alt  {{ com Constructor applied to fresh names }}
 
-tick :: 'Tickish_' ::= {{ com Internal notes, \coderef{coreSyn/CoreSyn.hs}{Tickish} }}
+tick :: 'Tickish_' ::= {{ com Internal notes, \coderef{GHC/Core.hs}{Tickish} }}
 
-Kp {{ tex \mathbb{K} }} :: 'AltCon_' ::= {{ com Constructors used in patterns, \coderef{coreSyn/CoreSyn.hs}{AltCon} }}
+Kp {{ tex \mathbb{K} }} :: 'AltCon_' ::= {{ com Constructors used in patterns, \coderef{GHC/Core.hs}{AltCon} }}
   | K        ::   :: DataAlt         {{ com \ctor{DataAlt}: Data constructor }}
   | lit      ::   :: LitAlt          {{ com \ctor{LitAlt}: Literal (such as an integer or character) }}
   | _        ::   :: DEFAULT         {{ com \ctor{DEFAULT}: Wildcard }}
 
-program :: 'CoreProgram_' ::= {{ com A System FC program, \coderef{coreSyn/CoreSyn.hs}{CoreProgram} }}
+program :: 'CoreProgram_' ::= {{ com A System FC program, \coderef{GHC/Core.hs}{CoreProgram} }}
   | </ bindingi // i />  ::   :: CoreProgram  {{ com List of bindings }}
 
 %% TYPES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}, phi {{ tex \phi }}
-  :: 'Type_' ::= {{ com Types/kinds, \coderef{types/TyCoRep.hs}{Type} }}
+  :: 'Type_' ::= {{ com Types/kinds, \coderef{GHC/Core/TyCo/Rep.hs}{Type} }}
   | n                       ::   :: TyVarTy       {{ com \ctor{TyVarTy}: Variable }}
   | t1 t2                   ::   :: AppTy         {{ com \ctor{AppTy}: Application }}
   | T </ ti // i />         ::   :: TyConApp      {{ com \ctor{TyConApp}: Application of type constructor }}
@@ -118,12 +118,12 @@ t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}, phi {{ tex \phi }}
   | lit                     ::   :: LitTy         {{ com \ctor{LitTy}: Type-level literal }}
   | t |> g                  ::   :: CastTy        {{ com \ctor{CastTy}: Kind cast }}
   | g                       ::   :: CoercionTy    {{ com \ctor{CoercionTy}: Coercion used in type }}
-  | tyConKind T             :: M :: tyConKind     {{ com \coderef{types/TyCon.hs}{tyConKind} }}
+  | tyConKind T             :: M :: tyConKind     {{ com \coderef{GHC/Core/TyCon.hs}{tyConKind} }}
   | t1 k1 ~# k2 t2          :: M :: unliftedEq    {{ com Metanotation for coercion types }}
     {{ tex [[t1]] \mathop{ {}^{[[k1]]}\!\! \sim_{\#}^{[[k2]]} } [[t2]] }}
   | t1 k1 ~Rep# k2 t2         :: M :: unliftedREq   {{ com Metanotation for coercion types }}
     {{ tex [[t1]] \mathop{ {}^{[[k1]]}\!\! \sim_{\mathsf{R}\#}^{[[k2]]} } [[t2]] }}
-  | literalType lit         :: M :: literalType   {{ com \coderef{basicTypes/Literal.hs}{literalType} }}
+  | literalType lit         :: M :: literalType   {{ com \coderef{GHC/Types/Literal.hs}{literalType} }}
   | ( t )                   :: M :: parens        {{ com Parentheses }}
   | { t }                   :: M :: IParens       {{ com Invisible parentheses }}
     {{ tex [[t]] }}
@@ -137,7 +137,7 @@ t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}, phi {{ tex \phi }}
 
 %% COERCIONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coderef{types/TyCoRep.hs}{Coercion} }}
+g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coderef{GHC/Core/TyCo/Rep.hs}{Coercion} }}
   | < t >                   ::   :: Refl          {{ com \ctor{Refl}: Nominal Reflexivity }}
     {{ tex {\langle [[t]] \rangle} }}
   | < t > R mg              ::   :: GRefl         {{ com \ctor{GRefl}: Generalized Reflexivity }}
@@ -165,7 +165,7 @@ g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coder
   | t $ liftingsubst        :: M :: Lifted        {{ com Type lifted to coercion }}
   | downgradeRole R g       :: M :: downgradeRole {{ com \textsf{downgradeRole} }}
 
-prov :: 'UnivCoProvenance_' ::= {{ com \ctor{UnivCo} provenance, \coderef{types/TyCoRep.hs}{UnivCoProvenance} }}
+prov :: 'UnivCoProvenance_' ::= {{ com \ctor{UnivCo} provenance, \coderef{GHC/Core/TyCo/Rep.hs}{UnivCoProvenance} }}
   | UnsafeCoerceProv   ::   :: UnsafeCoerceProv  {{ com From \texttt{unsafeCoerce\#} }}
     {{ tex \mathsf{unsafe} }}
   | PhantomProv        ::   :: PhantomProv       {{ com From the need for a phantom coercion }}
@@ -173,20 +173,20 @@ prov :: 'UnivCoProvenance_' ::= {{ com \ctor{UnivCo} provenance, \coderef{types/
   | ProofIrrelProv     ::   :: ProofIrrelProv    {{ com From proof irrelevance }}
     {{ tex \mathsf{irrel} }}
 
-mg {{ tex m }} :: 'MCoercion_' ::= {{ com A possibly reflexive coercion , \coderef{types/TyCoRep.hs}{MCoercion} }}
+mg {{ tex m }} :: 'MCoercion_' ::= {{ com A possibly reflexive coercion , \coderef{GHC/Core/TyCo/Rep.hs}{MCoercion} }}
   | MRefl            ::   :: MRefl                {{ com \ctor{MRefl}: A trivial reflexive coercion }}
   | MCo g            ::   :: MCo                  {{ com \ctor{MCo}: Other coercions }}
     {{ tex [[g]] }}
 
-LorR :: 'LeftOrRight_' ::= {{ com left or right deconstructor, \coderef{types/TyCoRep.hs}{LeftOrRight} }}
+LorR :: 'LeftOrRight_' ::= {{ com left or right deconstructor, \coderef{GHC/Core/TyCo/Rep.hs}{LeftOrRight} }}
   | Left             ::   :: CLeft                {{ com \ctor{CLeft}: Left projection }}
   | Right            ::   :: CRight               {{ com \ctor{CRight}: Right projection }}
 
-C :: 'CoAxiom_' ::= {{ com Axioms, \coderef{types/TyCon.hs}{CoAxiom} }}
+C :: 'CoAxiom_' ::= {{ com Axioms, \coderef{GHC/Core/TyCon.hs}{CoAxiom} }}
   | T RA </ axBranchi // ; // i />     ::   :: CoAxiom  {{ com \ctor{CoAxiom}: Axiom }}
   | ( C )                              :: M :: Parens   {{ com Parentheses }}
 
-R {{ tex \rho }} :: 'Role_' ::= {{ com Roles, \coderef{types/CoAxiom.hs}{Role} }}
+R {{ tex \rho }} :: 'Role_' ::= {{ com Roles, \coderef{GHC/Core/Coercion/Axiom.hs}{Role} }}
   | Nom              ::   :: Nominal              {{ com Nominal }}
     {{ tex \mathsf{N} }}
   | Rep              ::   :: Representational     {{ com Representational }}
@@ -195,17 +195,17 @@ R {{ tex \rho }} :: 'Role_' ::= {{ com Roles, \coderef{types/CoAxiom.hs}{Role} }
     {{ tex \mathsf{P} }}
   | role_list [ i ]  :: M :: RoleListIndex        {{ com Look up in list }}
 
-axBranch, b :: 'CoAxBranch_' ::= {{ com Axiom branches, \coderef{types/TyCon.hs}{CoAxBranch} }}
+axBranch, b :: 'CoAxBranch_' ::= {{ com Axiom branches, \coderef{GHC/Core/TyCon.hs}{CoAxBranch} }}
   | forall </ ni RAi // i /> . ( </ tj // j /> ~> s )  ::   :: CoAxBranch  {{ com \ctor{CoAxBranch}: Axiom branch }}
   | ( </ axBranchi // i /> ) [ ind ]               :: M :: lookup      {{ com List lookup }}
 
-mu {{ tex \mu }} :: 'CoAxiomRule_' ::= {{ com CoAxiomRules, \coderef{types/CoAxiom.hs}{CoAxiomRule} }}
+mu {{ tex \mu }} :: 'CoAxiomRule_' ::= {{ com CoAxiomRules, \coderef{GHC/Core/Coercion/Axiom.hs}{CoAxiomRule} }}
   | M ( I , role_list , R' )   ::  :: CoAxiomRule  {{ com Named rule, with parameter info }}
     {{ tex {[[M]]}_{([[I]], [[ role_list ]], [[R']])} }}
 
 %% TYCONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-T :: 'TyCon_' ::= {{ com Type constructors, \coderef{types/TyCon.hs}{TyCon} }}
+T :: 'TyCon_' ::= {{ com Type constructors, \coderef{GHC/Core/TyCon.hs}{TyCon} }}
   | ( -> )       ::   :: FunTyCon          {{ com \ctor{FunTyCon}: Arrow }}
 
   % the following also includes TupleTyCon, SynTyCon
@@ -226,22 +226,22 @@ H :: 'PrimTyCon_' ::= {{ com Primitive type constructors, \coderef{GHC.Builtin.T
   | TYPE         ::   :: TYPE                   {{ com TYPE (\texttt{tYPETyCon}) }}
   | Levity       ::   :: Levity                 {{ com Levity (\texttt{LevityTyCon}) }}
 
-K :: 'DataCon_' ::= {{ com Data constructors, \coderef{basicTypes/DataCon.hs}{DataCon} }}
+K :: 'DataCon_' ::= {{ com Data constructors, \coderef{GHC/Core/DataCon.hs}{DataCon} }}
   | Lifted       ::   :: Lifted       {{ com \ctor{Lifted}, a lifted type }}
   | Unlifted     ::   :: Unlifted     {{ com \ctor{Unlifted}, an unlifted type }}
 
 %% CONTEXTS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-G {{ tex \Gamma }} :: 'LintM_Bindings_' ::= {{ com List of bindings, \coderef{coreSyn/CoreLint.hs}{LintM} }}
+G {{ tex \Gamma }} :: 'LintM_Bindings_' ::= {{ com List of bindings, \coderef{GHC/Core/Lint.hs}{LintM} }}
   | n                        ::   :: Binding   {{ com Single binding }}
   | </ Gi // , // i />       ::   :: Concat    {{ com Context concatenation }}
-  | vars_of binding          :: M :: VarsOf    {{ com \coderef{coreSyn/CoreSyn.hs}{bindersOf} }}
+  | vars_of binding          :: M :: VarsOf    {{ com \coderef{GHC/Core.hs}{bindersOf} }}
 
-D {{ tex \Delta }} :: 'LintM_JoinBindings_' ::= {{ com List of join bindings, \coderef{coreSyn/CoreLint.hs}{LintM} }}
+D {{ tex \Delta }} :: 'LintM_JoinBindings_' ::= {{ com List of join bindings, \coderef{GHC/Core/Lint.hs}{LintM} }}
   | l                        ::   :: Binding   {{ com Single binding }}
   | </ Di // , // i />       ::   :: Concat    {{ com Context concatenation }}
   | empty                    :: M :: Empty     {{ com Empty context }}
-  | labels_of binding        :: M :: LabelsOf  {{ com \coderef{coreSyn/CoreSyn.hs}{bindersOf} }}
+  | labels_of binding        :: M :: LabelsOf  {{ com \coderef{GHC/Core.hs}{bindersOf} }}
 
 O {{ tex \Omega }} :: 'VarEnv_Role_' ::= {{ com Mapping from type variables to roles }}
   | </ ni : Ri // i />       ::   :: List      {{ com List of bindings }}
diff --git a/docs/core-spec/README b/docs/core-spec/README
index db864338c6..b50189a05e 100644
--- a/docs/core-spec/README
+++ b/docs/core-spec/README
@@ -30,7 +30,7 @@ into LaTeX math-mode code. Thus, the file core-spec.mng is the source for
 core-spec.tex, which gets processed into core-spec.pdf.
 
 The file CoreSyn.ott contains the grammar of System FC, mostly extracted from
-compiler/coreSyn/CoreSyn.hs. Here are a few pointers to help those of you
+compiler/GHC/Core.hs. Here are a few pointers to help those of you
 unfamiliar with Ott:
 
 - The {{ ... }} snippets are called "homs", and they assist ott in translating
@@ -69,7 +69,7 @@ your notation to LaTeX. Three different homs are used:
   it if necessary to disambiguate other parses.
 
 The file CoreLint.ott contains inductively defined judgements for many of the
-functions in compiler/coreSyn/CoreLint.hs. Each judgement is labeled with an
+functions in compiler/GHC/Core/Lint.hs. Each judgement is labeled with an
 abbreviation to distinguish it from the others. These abbreviations appear in
 the source code right after a turnstile |-. The declaration for each judgment
 contains a reference to the function it represents. Each rule is labeled with
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index d5262743e7..18a856f4e6 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -31,7 +31,7 @@ System FC, as implemented in GHC\footnote{This
 document was originally prepared by Richard Eisenberg (\texttt{eir@cis.upenn.edu}),
 but it should be maintained by anyone who edits the functions or data structures
 mentioned in this file. Please feel free to contact Richard for more information.}\\
-\Large 26 January, 2018
+\Large 26 May, 2020
 \end{center}
 
 \section{Introduction}
@@ -72,8 +72,8 @@ Literals do not play a major role, so we leave them abstract:
 
 \gram{\ottlit}
 
-We also leave abstract the function \coderef{basicTypes/Literal.hs}{literalType}
-and the judgment \coderef{coreSyn/CoreLint.hs}{lintTyLit} (written $[[G |-tylit lit : k]]$).
+We also leave abstract the function \coderef{GHC/Types/Literal.hs}{literalType}
+and the judgment \coderef{GHC/Core/Lint.hs}{lintTyLit} (written $[[G |-tylit lit : k]]$).
 
 \subsection{Variables}
 \enlargethispage{10pt} % without this first line of "z" definition is placed on
@@ -351,13 +351,13 @@ fresh in the context. In the implementation, of course, some work is done
 to guarantee this freshness. In particular, adding a new type variable to
 the context sometimes requires creating a new, fresh variable name and then
 applying a substitution. We elide these details in this formalism, but
-see \coderef{types/Type.hs}{substTyVarBndr} for details.
+see \coderef{GHC/Core/Type.hs}{substTyVarBndr} for details.
 
 \section{Typing judgments}
 
 The following functions are used from GHC. Their names are descriptive, and they
-are not formalized here: \coderef{types/TyCon.hs}{tyConKind},
-\coderef{types/TyCon.hs}{tyConArity}, \coderef{basicTypes/DataCon.hs}{dataConTyCon}, \coderef{types/TyCon.hs}{isNewTyCon}, \coderef{basicTypes/DataCon.hs}{dataConRepType}.
+are not formalized here: \coderef{GHC/Core/TyCon.hs}{tyConKind},
+\coderef{GHC/Core/TyCon.hs}{tyConArity}, \coderef{GHC/Core/DataCon.hs}{dataConTyCon}, \coderef{GHC/Core/TyCon.hs}{isNewTyCon}, \coderef{GHC/Core/DataCon.hs}{dataConRepType}.
 
 \subsection{Program consistency}
 
@@ -367,7 +367,7 @@ and then check each binding.
 
 \ottdefnlintCoreBindings{}
 
-Here is the definition of $[[vars_of]]$, taken from \coderef{coreSyn/CoreSyn.hs}{bindersOf}:
+Here is the definition of $[[vars_of]]$, taken from \coderef{GHC/Core.hs}{bindersOf}:
 
 \[
 \begin{array}{ll}
@@ -413,11 +413,11 @@ to check each substituted type $[[s'i]]$ in a context containing all the types
 that come before it in the list of bindings. The $[[G'i]]$ are contexts
 containing the names and kinds of all type variables (and term variables,
 for that matter) up to the $i$th binding. This logic is extracted from
-\coderef{coreSyn/CoreLint.hs}{lintAndScopeIds}.
+\coderef{GHC/Core/Lint.hs}{lintAndScopeIds}.
 
 \item The GHC source code checks all arguments in an application expression
-all at once using \coderef{coreSyn/CoreSyn.hs}{collectArgs}
-and \coderef{coreSyn/CoreLint.hs}{lintCoreArgs}. The operation
+all at once using \coderef{GHC/Core.hs}{collectArgs}
+and \coderef{GHC/Core/Lint.hs}{lintCoreArgs}. The operation
 has been unfolded for presentation here.
 
 \item If a $[[tick]]$ contains breakpoints, the GHC source performs additional
@@ -481,7 +481,7 @@ We believe both technical approaches are equivalent in what coercions they accep
 \label{sec:name_consistency}
 
 There are three very similar checks for names, two performed as part of
-\coderef{coreSyn/CoreLint.hs}{lintSingleBinding}:
+\coderef{GHC/Core/Lint.hs}{lintSingleBinding}:
 
 \ottdefnlintSingleBindingXXlintBinder{}
 
@@ -565,12 +565,12 @@ The judgment $[[apart]]$ checks to see whether two lists of types are surely
 apart. $[[apart( </ ti // i />, </ si // i /> )]]$, where $[[ </ ti // i />
 ]]$ is a list of types and $[[ </ si // i /> ]]$ is a list of type
 \emph{patterns} (as in a type family equation), first flattens the $[[ </ ti
-    // i /> ]]$ using \coderef{types/FamInstEnv.hs}{flattenTys} and then checks to
-see if \coderef{types/Unify.hs}{tcUnifyTysFG} returns \texttt{SurelyApart}.
+    // i /> ]]$ using \coderef{GHC/Core/FamInstEnv.hs}{flattenTys} and then checks to
+see if \coderef{GHC/Core/Unify.hs}{tcUnifyTysFG} returns \texttt{SurelyApart}.
 Flattening takes all type family applications and replaces them with fresh variables,
 taking care to map identical type family applications to the same fresh variable.
 
-The algorithm $[[unify]]$ is implemented in \coderef{types/Unify.hs}{tcUnifyTys}.
+The algorithm $[[unify]]$ is implemented in \coderef{GHC/Core/Unify.hs}{tcUnifyTys}.
 It performs a standard unification, returning a substitution upon success.
 
 \section{Operational semantics}
@@ -579,7 +579,7 @@ It performs a standard unification, returning a substitution upon success.
 GHC does not implement an operational semantics in any concrete form. Most
 of the rules below are implied by algorithms in, for example, the simplifier
 and optimizer. Yet, there is no one place in GHC that states these rules,
-analogously to \texttt{CoreLint.hs}.
+analogously to \texttt{GHC/Core/Lint.hs}.
 Nevertheless, these rules are included in this document to help the reader
 understand System FC.
 
@@ -607,17 +607,17 @@ to the constructor. The terms are the regular term arguments stored in an
 algebraic datatype. Coercions (say, in a GADT) are considered term arguments.
 \item The rule \ottdrulename{S\_CasePush} is the most complex rule.
 \begin{itemize}
-\item The logic in this rule is implemented in \coderef{coreSyn/CoreSubst.hs}{exprIsConApp\_maybe}.
-\item The $[[coercionKind]]$ function (\coderef{types/Coercion.hs}{coercionKind})
+\item The logic in this rule is implemented in \coderef{GHC/Core/Subst.hs}{exprIsConApp\_maybe}.
+\item The $[[coercionKind]]$ function (\coderef{GHC/Core/Coercion.hs}{coercionKind})
 extracts the two types (and their kinds) from
 a coercion. It does not require a typing context, as it does not \emph{check} the
 coercion, just extracts its types.
-\item The $[[dataConRepType]]$ function (\coderef{basicTypes/DataCon.hs}{dataConRepType}) extracts the full type of a data constructor. Following the notation for
+\item The $[[dataConRepType]]$ function (\coderef{GHC/Core/DataCon.hs}{dataConRepType}) extracts the full type of a data constructor. Following the notation for
 constructor expressions, the parameters to the constructor are broken into three
 groups: universally quantified types, existentially quantified types, and terms.
 \item The substitutions in the last premise to the rule are unusual: they replace
 \emph{type} variables with \emph{coercions}. This substitution is called lifting
-and is implemented in \coderef{types/Coercion.hs}{liftCoSubst}. The notation is
+and is implemented in \coderef{GHC/Core/Coercion.hs}{liftCoSubst}. The notation is
 essentially a pun on the fact that types and coercions have such similar structure.
 This operation is quite non-trivial. Please see \emph{System FC with Explicit
 Kind Equality} for details.
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index 75bb620edc..97da6c89f1 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf