grammar: rename At -> Sourced

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

diff --git a/symantic-lib/Language/Symantic/Lib/Maybe.hs b/symantic-lib/Language/Symantic/Lib/Maybe.hs
index 561ede9634b28392abfa8b9d77d0176cc3db6b80..12093fce4a8f76ac2553b13ab79a6dfeb7a81461 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Maybe.hs
+++ b/symantic-lib/Language/Symantic/Lib/Maybe.hs
@@ -45,34 +45,36 @@ instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (Dup r1 r2) where
 instance (Sym_Maybe term, Sym_Lambda term) => Sym_Maybe (BetaT term)
 
 -- Typing
+instance NameTyOf Maybe where
+       nameTyOf _c = ["Maybe"] `Mod` "Maybe"
 instance FixityOf Maybe
 instance ClassInstancesFor Maybe where
-       proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
-        | Just HRefl <- proj_ConstKiTy @_ @Maybe c
+       proveConstraintFor _ (TyConst _ _ q :$ m)
+        | Just HRefl <- proj_ConstKiTy @_ @Maybe m
         = case () of
                 _ | Just Refl <- proj_Const @Applicative q -> Just Dict
-                  | Just Refl <- proj_Const @Foldable q    -> Just Dict
-                  | Just Refl <- proj_Const @Functor q     -> Just Dict
-                  | Just Refl <- proj_Const @Monad q       -> Just Dict
+                  | Just Refl <- proj_Const @Foldable    q -> Just Dict
+                  | Just Refl <- proj_Const @Functor     q -> Just Dict
+                  | Just Refl <- proj_Const @Monad       q -> Just Dict
                   | Just Refl <- proj_Const @Traversable q -> Just Dict
                 _ -> Nothing
-       proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))
-        | Just HRefl <- proj_ConstKiTy @_ @Maybe c
+       proveConstraintFor _ (tq@(TyConst _ _ q) :$ m:@a)
+        | Just HRefl <- proj_ConstKiTy @_ @Maybe m
         = case () of
                 _ | Just Refl <- proj_Const @Eq q
-                  , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
                   | Just Refl <- proj_Const @Monoid q
-                  , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
                   | Just Refl <- proj_Const @Show q
-                  , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
                   | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
                   | Just Refl <- proj_Const @MT.MonoFunctor q  -> Just Dict
                 _ -> Nothing
        proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor Maybe where
-       expandFamFor _c _len f (TyApp _ c a `TypesS` TypesZ)
+       expandFamFor _c _len f (m:@a `TypesS` TypesZ)
         | Just HRefl <- proj_ConstKi @_ @Element f
-        , Just HRefl <- proj_ConstKiTy @_ @Maybe c
+        , Just HRefl <- proj_ConstKiTy @_ @Maybe m
         = Just a
        expandFamFor _c _len _fam _as = Nothing