Remove dependency on ghc-prim.

[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Unit.hs

diff --git a/symantic-lib/Language/Symantic/Lib/Unit.hs b/symantic-lib/Language/Symantic/Lib/Unit.hs
index c260e61d05f43276e6659f2e0a503010766d9a28..573afc294eb9431db91f39578698186ff3ca1915 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Unit.hs
+++ b/symantic-lib/Language/Symantic/Lib/Unit.hs
@@ -9,7 +9,7 @@ import Language.Symantic
 import Language.Symantic.Grammar
 
 -- * Class 'Sym_Unit'
-type instance Sym (Proxy ()) = Sym_Unit
+type instance Sym () = Sym_Unit
 class Sym_Unit term where
        unit :: term ()
        default unit :: Sym_Unit (UnT term) => Trans term => term ()
@@ -27,6 +27,8 @@ instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (Dup r1 r2) where
 instance (Sym_Unit term, Sym_Lambda term) => Sym_Unit (BetaT term)
 
 -- Typing
+instance NameTyOf () where
+       nameTyOf _c = [] `Mod` ""
 instance ClassInstancesFor () where
        proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
         | Just HRefl <- proj_ConstKiTy @_ @() z
@@ -46,11 +48,11 @@ instance
  ( Gram_Source src g
  , Gram_Rule g
  , Gram_Comment g
- , Inj_Sym ss ()
+ , SymInj ss ()
  ) => Gram_Term_AtomsFor src ss g () where
-       g_term_atomsFor _t =
+       g_term_atomsFor =
         [ rule "teUnit" $
-               g_source $
+               source $
                (\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teUnit)
                 <$ symbol "("
                 <* symbol ")"
@@ -58,11 +60,9 @@ instance
 instance ModuleFor src ss ()
 
 -- ** 'Type's
-tyUnit :: Source src => Inj_Len vs => Type src vs ()
+tyUnit :: Source src => LenInj vs => Type src vs ()
 tyUnit = tyConst @(K ()) @()
 
 -- ** 'Term's
-teUnit ::
- Source src => Inj_Sym ss () =>
- Term src ss ts '[] ()
+teUnit :: TermDef () '[] (() #> ())
 teUnit = Term noConstraint tyUnit $ teSym @() $ unit