stack: bump to lts-12.25

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

diff --git a/symantic-lib/Language/Symantic/Lib/NonNull.hs b/symantic-lib/Language/Symantic/Lib/NonNull.hs
index 607eba7e18db7b2db62ab7c93af27f47756c056f..1f8753c6b16d7a2b406beeb3a6aff06d6507f519 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/NonNull.hs
+++ b/symantic-lib/Language/Symantic/Lib/NonNull.hs
@@ -19,7 +19,7 @@ import Language.Symantic.Lib.Sequences (tySemiSequence, tyIsSequence, s0)
 import Language.Symantic.Lib.Tuple2 (tyTuple2)
 
 -- * Class 'Sym_NonNull'
-type instance Sym (Proxy NonNull) = Sym_NonNull
+type instance Sym NonNull = Sym_NonNull
 class Sym_NonNull term where
        fromNullable :: MonoFoldable o => term o -> term (Maybe (NonNull o))
        toNullable   :: MonoFoldable o => term (NonNull o) -> term o
@@ -85,35 +85,37 @@ instance (Sym_NonNull r1, Sym_NonNull r2) => Sym_NonNull (Dup r1 r2) where
 instance (Sym_NonNull term, Sym_Lambda term) => Sym_NonNull (BetaT term)
 
 -- Typing
+instance NameTyOf NonNull where
+       nameTyOf _c = ["NonNull"] `Mod` "NonNull"
 instance FixityOf NonNull
 instance TypeInstancesFor NonNull where
-       expandFamFor c len f (TyApp _ z o `TypesS` TypesZ)
+       expandFamFor c len f (z:@o `TypesS` TypesZ)
         | Just HRefl <- proj_ConstKi @_ @Element f
         , Just HRefl <- proj_ConstKiTy @_ @NonNull z
         = expandFamFor c len f (o `TypesS` TypesZ)
        expandFamFor _c _len _fam _as = Nothing
 instance ClassInstancesFor NonNull where
-       proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c o))
+       proveConstraintFor _ (tq@(TyConst _ _ q) :$ c:@o)
         | Just HRefl <- proj_ConstKiTy @_ @NonNull c
         = case () of
                 _ | Just Refl <- proj_Const @Eq q
-                  , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict
                   | Just Refl <- proj_Const @MT.MonoFoldable q
-                  , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict
                   | Just Refl <- proj_Const @MT.MonoFunctor q
-                  , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict
                   | Just Refl <- proj_Const @Ord q
-                  , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict
                   | Just Refl <- proj_Const @SemiSequence q
-                  , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict
                   | Just Refl <- proj_Const @Show q
-                  , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict
                 _ -> Nothing
        proveConstraintFor _c _q = Nothing
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g NonNull
-instance (Source src, Inj_Sym ss NonNull) => ModuleFor src ss NonNull where
+instance (Source src, SymInj ss NonNull) => ModuleFor src ss NonNull where
        moduleFor = ["NonNull"] `moduleWhere`
         [ "fromNullable" := teNonNull_fromNullable
         , "toNullable"   := teNonNull_toNullable