vlopezj

This is an explanation of the changes introduced in pull request agda/agda#5234

Twin context infrastructure

When checking whether two well-typed terms t and u are convertible, they might not be typed in the same context.

From the example above, we have a constraint

vlopezj

Monad gives Applicative, Applicative etc. gives Num, Floating, Fractional

Setting it up

WrapMonad tells us that a Monad implies Functor, Applicative

instance Monad m => Functor     (WrappedMonad m)
instance Monad m => Applicative (WrappedMonad m)
instance Monad m => Monad       (WrappedMonad m)

vlopezj

data EitherDup a = MyLeft a
                 | MyRight a

class HasEndo t where
  -- | prop>  endo . endo == id
  endo :: t -> t
  
instance HasEndo (EitherDup a) where
  endo (MyLeft a) = MyRight a
  endo (MyRight a) = MyLeft a

vlopezj

agda

module FunImplicits where

open import Data.Bool

data Nat : Set where
  zero : Nat