Prefer GADT's over typ families for some SyntaxTree elements.

1 files changed, 13 insertions, 23 deletions

diff --git a/src/Language/Fiddle/Ast/Internal/SyntaxTree.hs b/src/Language/Fiddle/Ast/Internal/SyntaxTree.hs
index 9566ab5..66b8e42 100644
--- a/src/Language/Fiddle/Ast/Internal/SyntaxTree.hs
+++ b/src/Language/Fiddle/Ast/Internal/SyntaxTree.hs
@@ -9,7 +9,6 @@
 module Language.Fiddle.Ast.Internal.SyntaxTree
   ( -- Type Families
     NumberType,
-    ImportInterface,
     FiddleUnitInterface,
     QualificationMetadata,
     CommonQualificationData (..),
@@ -64,7 +63,11 @@ import GHC.Generics
 import Language.Fiddle.Ast.Internal.Instances
 import Language.Fiddle.Ast.Internal.Kinds
 import Language.Fiddle.Ast.Internal.Stage
+import Language.Fiddle.Ast.Internal.MetaTypes
 import Language.Fiddle.Internal.UnitInterface
+import Data.Type.Equality
+import GHC.TypeError as TypeError
+import GHC.TypeLits
 
 -- | Common data for each qualified element.
 newtype CommonQualificationData
@@ -80,37 +83,24 @@ type BitsOffset stage = RegisterOffset stage
 -- stage, which will attach the appropriate offset to the register. This helps
 -- backends so they don't have to recalculate this offset.
 type family RegisterOffset stage where
-  RegisterOffset stage = If (stage < Checked) () Word32
+  RegisterOffset stage = If (stage .< Checked) () Word32
 
 -- | Type which stores metadata after qualification. Before qualification, this
 -- metadata has not been calculated and so is unset.
 type family QualificationMetadata stage t where
   QualificationMetadata stage t =
-    If (stage < Qualified) () t
+    If (stage .< Qualified) () t
 
 -- | The type attached to import statements which describe the imported file's
 -- unit interface
 type family FiddleUnitInterface (s :: Stage) :: Type where
-  FiddleUnitInterface s = If (s < Checked) () UnitInterface
+  FiddleUnitInterface s = If (s .< Checked) () UnitInterface
 
 -- | The Type of number during each stage of compilation. When in the first stage,
 -- numbers are just strings like anything else. In later stages, numbers get
 -- parsed into actual integers. This makes it easier to process later.
 type family NumberType (a :: Stage) :: Type where
-  NumberType s = If (s < Expanded) Text Integer
-
--- | The type used for ImportInterfaces attached to ImportStatements. Before import
--- resolution, this type is just '()', but when imports are resolved, it turns
--- into a 'UnitInterface'.
-type family ImportInterface (stage :: Stage) :: Type where
-  ImportInterface s = If (s < ImportsResolved) () UnitInterface
-
--- | A type which is only constructible if the type-level condition 's' holds.
---
--- This type is used as a way to enable/disable parts of the syntax tree based
--- on type level booleans (typically incorporating the compilation 'stage') 
-data Witness (s :: Bool) where
-  Witness :: Witness True
+  NumberType s = If (s .< Expanded) Text Integer
 
 -- A Name is multiple identifiers separated by dots. It's the way of namespaces
 -- to different packages.
@@ -249,7 +239,7 @@ data FiddleUnit (stage :: Stage) (f :: Type -> Type) a where
   FiddleUnit ::
     { -- | The interface for this FiddleUnit. Early on, this is just () because
       -- not enough information is provided to determine the interface..
-      fiddleUnitInterface :: FiddleUnitInterface stage,
+      fiddleUnitInterface :: When (stage == Checked) UnitInterface,
       -- | List of declarations.
       fiddleDecls :: [Directed FiddleDecl stage f a],
       -- | Annotation for the 'FiddleUnit'.
@@ -294,7 +284,7 @@ data ImportStatement stage f a where
       importPath :: Text,
       -- | Optional list of imported items.
       importList :: Maybe (ImportList f a),
-      importInterface :: ImportInterface stage,
+      importInterface :: When (stage .>= ImportsResolved) UnitInterface,
       -- | Annotation for the import statement.
       importStatementAnnot :: a
     } ->
@@ -433,7 +423,7 @@ data ObjType stage f a where
   -- | An anonymous object type, allowed only in Parsed.
   AnonymousObjType ::
     { -- | Witness for stage constraint.
-      disableAnonymousTypesAfterExpansion :: Witness (stage < Expanded),
+      disableAnonymousTypesAfterExpansion :: Witness (stage .< Expanded),
       -- | The body of the anonymous type.
       anonBody :: f (ObjTypeBody stage f a),
       -- | Annotation for the anonymous type.
@@ -467,7 +457,7 @@ data ObjTypeDecl stage f a where
   -- | An assertion statement for a specific position.
   AssertPosStatement ::
     { -- | Witness for stage constraint.
-      disableAssertStatementsAfterConsistencyCheck :: Witness (stage < Checked),
+      disableAssertStatementsAfterConsistencyCheck :: Witness (stage .< Checked),
       -- | The expression for the assertion.
       assertExpr :: Expression stage f a,
       -- | Annotation for the assertion.
@@ -629,7 +619,7 @@ data RegisterBitsTypeRef stage f a where
   -- | An anonymous type for register bits, used in Parsed.
   RegisterBitsAnonymousType ::
     { -- | Witness for stage constraint.
-      disableAnonymousBitsAfterExpansion :: Witness (stage < Expanded),
+      disableAnonymousBitsAfterExpansion :: Witness (stage .< Expanded),
       -- | The anonymous type.
       anonBitsType :: AnonymousBitsType stage f a,
       -- | Annotation for the anonymous type.