Erasure monad vs. forced patterns, in Agda

er.agda

module er where

------------------------

data Erased (A : Set) : Set where
  E : A -> Erased A

pure : {A : Set} -> A -> Erased A
pure = E
  
infixl 3 _<$>_
_<$>_ : {A B : Set} -> (A -> B) -> Erased A -> Erased B
f <$> E x = E (f x)

infixl 3 _<*>_
_<*>_ : {A B : Set} -> Erased (A -> B) -> Erased A -> Erased B
E f <*> E x = E (f x)

-------------------------

data Unit : Set where
  tt : Unit

data Nat : Set where
  Z : Nat
  S : Nat -> Nat
  
inc : Nat -> Nat
inc    Z  = S Z
inc (S n) = S (inc n)

-------------------------

data T : Nat -> Set where
  C : (n : Nat) -> T (inc n)
  
g : (n : Nat) -> T n -> Unit
g .(inc n) (C n) = tt

data ET : Erased Nat -> Set where
  EC : (en : Erased Nat) -> ET (inc <$> en)
  
eg : (n : Nat) -> ET (pure n) -> Unit
eg n et = {!!}

{-

/home/ziman/er.agda:44,11-15
Cannot decide whether there should be a case for the constructor
EC, since the unification gets stuck on unifying the inferred
indices [inc <$> en] with the expected indices [E Z]
when checking that the expression ? has type Unit

-}