From 9fb42302e15b0cc4aae71e7d324d499c9f7f795f Mon Sep 17 00:00:00 2001 From: whatisRT Date: Mon, 14 Apr 2025 15:29:09 +0200 Subject: [PATCH] Small changes required by the new monad polymorphsm --- Class/Convertible/Core.agda | 4 ++-- Tactic/Derive/Convertible.agda | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Class/Convertible/Core.agda b/Class/Convertible/Core.agda index a64fd1d..e0d2af6 100644 --- a/Class/Convertible/Core.agda +++ b/Class/Convertible/Core.agda @@ -21,12 +21,12 @@ Convertible₁ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible (T A) Convertible₂ : (Set → Set → Set) → (Set → Set → Set) → Set₁ Convertible₂ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible₁ (T A) (U B) -Functor⇒Convertible : ∀ {F : Type↑} → ⦃ Functor F ⦄ → Convertible₁ F F +Functor⇒Convertible : ∀ {F : Type↑ id} → ⦃ Functor F ⦄ → Convertible₁ F F Functor⇒Convertible = λ where .to → fmap to .from → fmap from -Bifunctor⇒Convertible : ∀ {F} → ⦃ Bifunctor F ⦄ → Convertible₂ F F +Bifunctor⇒Convertible : ∀ {F : Type↑² (_⊔ˡ_)} → ⦃ Bifunctor F ⦄ → Convertible₂ F F Bifunctor⇒Convertible = λ where .to → bimap to to .from → bimap from from diff --git a/Tactic/Derive/Convertible.agda b/Tactic/Derive/Convertible.agda index 2269900..fce8525 100644 --- a/Tactic/Derive/Convertible.agda +++ b/Tactic/Derive/Convertible.agda @@ -24,7 +24,7 @@ open import Class.HasHsType open import Tactic.Derive.HsType private - instance _ = Functor-M {TC} + instance _ = Functor-M {_} {TC} open MonadReader ⦃...⦄