Upstream Convertible, HasHsType and their Deriving strategies

Class/Convertible.agda

@@ -0,0 +1,4 @@
+module Class.Convertible where
+
+open import Class.Convertible.Core public
+open import Class.Convertible.Instances public

Class/Convertible/Core.agda

@@ -0,0 +1,35 @@
+module Class.Convertible.Core where
+
+open import Meta.Prelude
+
+open import Class.Core
+open import Class.Functor
+open import Class.Bifunctor
+
+record Convertible (A B : Set) : Set where
+  field to   : A → B
+        from : B → A
+open Convertible ⦃...⦄ public
+
+Convertible-Refl : ∀ {A} → Convertible A A
+Convertible-Refl = λ where .to → id; .from → id
+
+Convertible₁ : (Set → Set) → (Set → Set) → Set₁
+Convertible₁ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible (T A) (U B)
+
+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 = λ where
+  .to   → fmap to
+  .from → fmap from
+
+Bifunctor⇒Convertible : ∀ {F} → ⦃ Bifunctor F ⦄ → Convertible₂ F F
+Bifunctor⇒Convertible = λ where
+  .to   → bimap to to
+  .from → bimap from from
+
+_⨾_ : ∀ {A B C} → Convertible A B → Convertible B C → Convertible A C
+(c ⨾ c') .to   = c' .to   ∘ c  .to
+(c ⨾ c') .from = c  .from ∘ c' .from

Class/Convertible/Instances.agda

@@ -0,0 +1,52 @@
+module Class.Convertible.Instances where
+
+open import Meta.Prelude
+
+open import Class.Functor
+open import Class.Bifunctor
+
+open import Class.Convertible.Core
+
+open import Class.HasHsType.Core
+
+HsConvertible : (A : Set) → ⦃ HasHsType A ⦄ → Set
+HsConvertible A = Convertible A (HsType A)
+
+open import Foreign.Haskell using (Pair; Either)
+open import Foreign.Haskell.Coerce using (coerce)
+
+instance
+  Convertible-ℕ : Convertible ℕ ℕ
+  Convertible-ℕ = λ where
+    .to   → id
+    .from → id
+
+  Convertible-Maybe : Convertible₁ Maybe Maybe
+  Convertible-Maybe = Functor⇒Convertible
+
+  Convertible-× : Convertible₂ _×_ _×_
+  Convertible-× = Bifunctor⇒Convertible
+
+  Convertible-Pair : Convertible₂ _×_ Pair
+  Convertible-Pair = λ where
+    .to   → coerce ∘ bimap to to
+    .from → bimap from from ∘ coerce
+
+  Convertible-⊎ : Convertible₂ _⊎_ _⊎_
+  Convertible-⊎ = Bifunctor⇒Convertible
+
+  Convertible-Either : Convertible₂ _⊎_ Either
+  Convertible-Either = λ where
+    .to   → coerce ∘ bimap to to
+    .from → bimap from from ∘ coerce
+
+  Convertible-List : Convertible₁ List List
+  Convertible-List = λ where
+    .to   → fmap to
+    .from → fmap from
+
+  Convertible-Fun : ∀ {A A' B B'} →
+    ⦃ Convertible A A' ⦄ → ⦃ Convertible B B' ⦄ → Convertible (A → B) (A' → B')
+  Convertible-Fun = λ where
+    .to   → λ f → to   ∘ f ∘ from
+    .from → λ f → from ∘ f ∘ to

Class/HasHsType.agda

@@ -0,0 +1,4 @@
+module Class.HasHsType where
+
+open import Class.HasHsType.Core public
+open import Class.HasHsType.Instances public

Class/HasHsType/Core.agda

@@ -0,0 +1,14 @@
+module Class.HasHsType.Core where
+
+open import Meta.Prelude
+
+record HasHsType (A : Set ℓ) : Set₁ where
+  field HsType : Set
+
+module _ (A : Set ℓ) where
+  mkHsType : Set → HasHsType A
+  mkHsType Hs .HasHsType.HsType = Hs
+
+  module _ ⦃ i : HasHsType A ⦄ where
+    HsType : Set
+    HsType = i .HasHsType.HsType

Class/HasHsType/Instances.agda

@@ -0,0 +1,32 @@
+module Class.HasHsType.Instances where
+
+open import Meta.Prelude
+
+open import Foreign.Haskell.Pair using (Pair)
+open import Foreign.Haskell.Either using (Either)
+
+open import Class.HasHsType.Core
+
+instance
+  iHsTy-ℕ      = mkHsType ℕ ℕ
+  iHsTy-Bool   = mkHsType Bool Bool
+  iHsTy-⊤      = mkHsType ⊤ ⊤
+  iHsTy-String = mkHsType String String
+
+-- TODO: macro for these kind of congruence instances
+module _ ⦃ _ : HasHsType A ⦄ where instance
+  iHsTy-List : HasHsType (List A)
+  iHsTy-List .HasHsType.HsType = List (HsType A)
+
+  iHsTy-Maybe : HasHsType (Maybe A)
+  iHsTy-Maybe .HasHsType.HsType = Maybe (HsType A)
+
+  module _ ⦃ _ : HasHsType B ⦄ where instance
+    iHsTy-Fun : HasHsType (A → B)
+    iHsTy-Fun .HasHsType.HsType = HsType A → HsType B
+
+    iHsTy-Sum : HasHsType (A ⊎ B)
+    iHsTy-Sum .HasHsType.HsType = Either (HsType A) (HsType B)
+
+    iHsTy-Pair : HasHsType (A × B)
+    iHsTy-Pair .HasHsType.HsType = Pair (HsType A) (HsType B)

Class/MonadError.agda

@@ -9,10 +9,7 @@ open import Reflection using (TC; ErrorPart; typeError; catchTC; strErr)
 
 module Class.MonadError where
 
-private
-  variable
-    e f : Level
-    A : Set f
+private variable e f : Level
 
 record MonadError (E : Set e) (M : ∀ {f} → Set f → Set f) : Setω where
   field

Class/MonadReader.agda

@@ -8,8 +8,6 @@ open import Class.Monad
 open import Class.Functor
 open import Class.MonadError
 
-private variable ℓ : Level
-
 open MonadError ⦃...⦄
 
 record MonadReader (R : Set ℓ) (M : ∀ {a} → Set a → Set a) ⦃ _ : Monad M ⦄ : Setω where

Class/MonadTC.agda

@@ -20,10 +20,6 @@ open import Class.Functor
 open import Class.Monad
 open import Class.Traversable
 
-private variable
-  a f : Level
-  A B : Set f
-
 data ReductionOptions : Set where
   onlyReduce : List Name → ReductionOptions
   dontReduce : List Name → ReductionOptions
@@ -73,7 +69,7 @@ record MonadTC (M : ∀ {f} → Set f → Set f)
                ⦃ m : Monad M ⦄ ⦃ me : MonadError (List ErrorPart) M ⦄ : Setω₁ where
   field
     unify            : Term → Term → M ⊤
-    typeError        : ∀ {A : Set f} → List ErrorPart → M A
+    typeError        : List ErrorPart → M A
     inferType        : Term → M Type
     checkType        : Term → Type → M Term
     normalise        : Term → M Term
@@ -227,7 +223,7 @@ module _ {M : ∀ {f} → Set f → Set f}
   open MonadTC mtc
   open MonadReader mre
 
-  record IsMErrorPart (A : Set a) : Setω where
+  record IsMErrorPart (A : Set ℓ) : Setω where
     field toMErrorPart : A → M (List ErrorPart)
 
   open IsMErrorPart ⦃...⦄ public

Meta/Prelude.agda

@@ -2,30 +2,45 @@
 
 module Meta.Prelude where
 
-open import Level renaming (_⊔_ to _⊔ˡ_; suc to sucˡ; zero to zeroˡ) public
+-- ** stdlib re-exports
+open import Level public
+  renaming (_⊔_ to _⊔ˡ_; suc to sucˡ; zero to zeroˡ)
 open import Function public
 
-open import Data.Bool hiding (_≟_; _≤_; _≤?_; _<_; _<?_) public
+open import Data.Bool public
+  hiding (_≟_; _≤_; _≤?_; _<_; _<?_)
 open import Data.Empty public
-open import Data.List hiding (align; alignWith; fromMaybe; map; zip; zipWith) public
-open import Data.Maybe hiding (_>>=_; ap; align; alignWith; fromMaybe; map; zip; zipWith) public
-open import Data.Unit hiding (_≟_) public
-open import Data.Sum hiding (assocʳ; assocˡ; map; map₁; map₂; reduce; swap) public
-open import Data.Product hiding (assocʳ; assocˡ; map; map₁; map₂; swap; zip; zipWith) public
-open import Data.Nat hiding (_≟_; _≤_; _≤?_; _<_; _<?_; _≤ᵇ_; _≡ᵇ_) public
-open import Data.String using (String; _<+>_) public
-
-open import Relation.Binary.PropositionalEquality hiding (preorder; setoid; [_]; module ≡-Reasoning; decSetoid) public
-
+open import Data.List public
+  hiding (align; alignWith; fromMaybe; map; zip; zipWith)
+open import Data.Maybe public
+  hiding (_>>=_; ap; align; alignWith; fromMaybe; map; zip; zipWith)
+open import Data.Unit public
+  hiding (_≟_)
+open import Data.Sum public
+  hiding (assocʳ; assocˡ; map; map₁; map₂; reduce; swap)
+open import Data.Product public
+  hiding (assocʳ; assocˡ; map; map₁; map₂; swap; zip; zipWith)
+open import Data.Nat public
+  hiding (_≟_; _≤_; _≤?_; _<_; _<?_; _≤ᵇ_; _≡ᵇ_)
+open import Data.String public
+  using (String; _<+>_)
+
+open import Relation.Binary.PropositionalEquality public
+  hiding (preorder; setoid; [_]; module ≡-Reasoning; decSetoid)
+
+-- ** helper funs
 lookupᵇ : {A B : Set} → (A → A → Bool) → List (A × B) → A → Maybe B
 lookupᵇ f [] n = nothing
 lookupᵇ f ((k , v) ∷ l) n = if f k n then just v else lookupᵇ f l n
 
-open import Data.Fin
-open import Data.List
-
 zipWithIndex : {A B : Set} → (ℕ → A → B) → List A → List B
 zipWithIndex f l = zipWith f (upTo $ length l) l
+  where open import Data.Fin; open import Data.List
 
 enumerate : {A : Set} → List A → List (ℕ × A)
 enumerate = zipWithIndex _,_
+
+-- ** variables
+variable
+  ℓ ℓ′ ℓ″ : Level
+  A B C D : Set ℓ

Reflection/AlphaEquality.agda

@@ -15,11 +15,6 @@ open import Relation.Binary            using (DecidableEquality)
 
 open import Class.DecEq
 
-private
-  variable
-    a : Level
-    A : Set a
-
 ------------------------------------------------------------------------
 -- Definition
 

Reflection/Debug.agda

@@ -13,11 +13,6 @@ open import Relation.Nullary.Decidable using (⌊_⌋)
 
 open import Reflection
 
-private
-  variable
-    a : Level
-    A : Set a
-
 record IsErrorPart (A : Set) : Set where
   field toErrorPart : A → ErrorPart
 

Reflection/TCI.agda

@@ -20,10 +20,7 @@ open import Class.MonadTC
 
 open Monad
 
-private variable a f : Level
-                 A B C D : Set a
-
-TC : Set a → Set a
+TC : Set ℓ → Set ℓ
 TC = ReaderT TCEnv R.TC
 
 Monad-TC : Monad TC
@@ -54,18 +51,17 @@ applyExtContext : Telescope → R.TC A → R.TC A
 applyExtContext [] x       = x
 applyExtContext (t ∷ ts) x = applyExtContext ts $ (uncurry R.extendContext) t x
 
-private
-  liftTC : R.TC A → TC A
-  liftTC x = λ r → applyExtContext (r .TCEnv.localContext) x
+liftTC : R.TC A → TC A
+liftTC x = λ r → applyExtContext (r .TCEnv.localContext) x
 
-  liftTC1 : (A → R.TC B) → A → TC B
-  liftTC1 f a = liftTC (f a)
+liftTC1 : (A → R.TC B) → A → TC B
+liftTC1 f a = liftTC (f a)
 
-  liftTC2 : (A → B → R.TC C) → A → B → TC C
-  liftTC2 f a b = liftTC (f a b)
+liftTC2 : (A → B → R.TC C) → A → B → TC C
+liftTC2 f a b = liftTC (f a b)
 
-  liftTC3 : (A → B → C → R.TC D) → A → B → C → TC D
-  liftTC3 f a b c = liftTC (f a b c)
+liftTC3 : (A → B → C → R.TC D) → A → B → C → TC D
+liftTC3 f a b c = liftTC (f a b c)
 
 module MonadTCI where
   unify             : Term → Term → TC ⊤

Reflection/Tactic.agda

@@ -13,10 +13,6 @@ open import Meta.Init
 
 open MonadTC ⦃...⦄
 
-private variable
-  a : Level
-  A : Set a
-
 Tactic = Term → R.TC ⊤
 UnquoteDecl = R.TC ⊤