Erasure monad vs. forced patterns

Er.hs

module Er

%default total

{- module Erasure; inlined for convenience -}

data Erased : Type -> Type where
  E : a -> Erased a

instance Functor Erased where
  map f (E x) = E (f x)

instance Applicative Erased where
  pure = E
  (<$>) (E f) (E x) = E (f x)

instance Monad Erased where
  (>>=) (E x) f = f x

liftEq : {a : Type} -> {x, y : a} -> x = y -> E x = E y
liftEq refl = refl

E_inj : {a : Type} -> {x, y : a} -> E x = E y -> x = y
E_inj refl = refl

{- module Main -}

f : Nat -> Nat
f n = n + 1

data T : Nat -> Type where
    C : (n : Nat) -> T (f n)

g : (n : Nat) -> T n -> ()
g (f n) (C n) = ()

data ET : Erased Nat -> Type where
    EC : (en : Erased Nat) -> ET [| f en |]

eg : (n : Nat) -> ET (pure n) -> ()
eg _ (EC en) = ()

{-

Type checking ./er.idr
er.idr:41:4:When elaborating left hand side of eg:
When elaborating an application of er.eg:
        Can't unify
                ET (Erased instance of Prelude.Applicative.Applicative, method <$> (E f)
                                                                                   en)
        with
                ET (pure n)
        
        Specifically:
                Can't unify
                        Erased instance of Prelude.Applicative.Applicative, method <$> (E f)
                                                                                       en
                with
                        E n
Metavariables: er.eg

-}