instance (Sym_Tuple2 term, Sym_Lambda term) => Sym_Tuple2 (BetaT term)
-- Typing
+instance NameTyOf (,) where
+ nameTyOf _c = ["Tuple2"] `Mod` ","
instance FixityOf (,) where
fixityOf _c = Just $ Fixity2 $ infixN (-1)
instance ClassInstancesFor (,) where
- proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c a))
- | Just HRefl <- proj_ConstKiTy @_ @(,) c
+ proveConstraintFor _ (TyConst _ _ q :$ t:@a)
+ | Just HRefl <- proj_ConstKiTy @_ @(,) t
= case () of
_ | Just Refl <- proj_Const @Applicative q
, Just Dict <- proveConstraint (tyMonoid a) -> Just Dict
, Just Dict <- proveConstraint (tyMonoid a) -> Just Dict
| Just Refl <- proj_Const @Traversable q -> Just Dict
_ -> Nothing
- proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c a) b))
- | Just HRefl <- proj_ConstKiTy @_ @(,) c
+ proveConstraintFor _ (tq@(TyConst _ _ q) :$ t:@a:@b)
+ | Just HRefl <- proj_ConstKiTy @_ @(,) t
= case () of
_ | Just Refl <- proj_Const @Bounded q
- , Just Dict <- proveConstraint (tq `tyApp` a)
- , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
+ , Just Dict <- proveConstraint (tq`tyApp`a)
+ , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
| Just Refl <- proj_Const @Eq q
- , Just Dict <- proveConstraint (tq `tyApp` a)
- , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
+ , Just Dict <- proveConstraint (tq`tyApp`a)
+ , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
| Just Refl <- proj_Const @Monoid q
- , Just Dict <- proveConstraint (tq `tyApp` a)
- , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
+ , Just Dict <- proveConstraint (tq`tyApp`a)
+ , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
| Just Refl <- proj_Const @Ord q
- , Just Dict <- proveConstraint (tq `tyApp` a)
- , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
+ , Just Dict <- proveConstraint (tq`tyApp`a)
+ , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
| Just Refl <- proj_Const @Show q
- , Just Dict <- proveConstraint (tq `tyApp` a)
- , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
+ , Just Dict <- proveConstraint (tq`tyApp`a)
+ , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
| Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
- | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict
+ | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict
_ -> Nothing
proveConstraintFor _c _q = Nothing
instance TypeInstancesFor (,) where
- expandFamFor _c _len f (TyApp _ (TyApp _ c _a) b `TypesS` TypesZ)
+ expandFamFor _c _len f (t:@_a:@b `TypesS` TypesZ)
| Just HRefl <- proj_ConstKi @_ @Element f
- , Just HRefl <- proj_ConstKiTy @_ @(,) c
+ , Just HRefl <- proj_ConstKiTy @_ @(,) t
= Just b
expandFamFor _c _len _fam _as = Nothing