Problem when compiling ".ss" file generated by idris

[redfish64]

zerobug.ipkg:
https://gist.github.com/redfish64/97329bf481996856f024c52cac4f87ad

ZeroBug.idr:
https://gist.github.com/redfish64/5c49eae1f3272c276a91da6f2a018e8f

Steps to Reproduce

idris2 --build zerobug.ipkg 

Expected Behavior

builds a working file.

Observed Behavior

1/1: Building ZeroBug (ZeroBug.idr)
Exception: attempt to reference unbound identifier pat0C-58-5 at line 582, char 756 of /home/tim/projects/idris2_learn/build/exec/zb_app/zb.ss

Sorry about the size of the example. It was deep in my code, and I had trouble tearing it out and still getting the issue to occur.

You can get the issue to disappear by commenting out line 83 and replacing it with line 82, here:

        -- => {0 s,a,k : Type} --replace the following line with this, and it compiles and runs fine
        => {s,a,k : Type} 

Here is the ipkg file to compile it:

package zerobug

depends = contrib

modules = ZeroBug
main = ZeroBug
executable = zb

And here is ZeroBug.idr:

module ZeroBug

import Control.Monad.Identity
import Data.Morphisms
import Data.SortedMap

public export
Optic : (Type -> Type -> Type) -> (Type -> Type) -> Type -> Type -> Type -> Type -> Type
Optic p f s t a b = p a (f b) -> p s (f t)

public export
Simple : (Type -> Type -> Type -> Type -> Type) -> Type -> Type -> Type
Simple p s a = p s s a a

public export
Optic' : (Type -> Type -> Type) -> (Type -> Type) -> Type -> Type -> Type
Optic' p f = Simple (Optic p f)

public export
LensLike : (Type -> Type) -> Type -> Type -> Type -> Type -> Type
LensLike = Optic Morphism

public export
LensLike' : (Type -> Type) -> Type -> Type -> Type
LensLike' f = Simple (LensLike f)

public export
data Const : (0 a : Type) -> (b : Type) -> Type where
  MkConst: a -> Const a b
  
public export
record OConst (0 m : Type -> Type) r v where
  constructor OConst_
  mv : m (Const r v)
  
public export
Functor m => Functor (OConst m r) where
  map f (OConst_ mv) = OConst_ (map (\(MkConst cv) => MkConst cv) mv)

public export
mapConst : Const r x -> Const r y
mapConst (MkConst {a = r} z) = MkConst {a=r} z

public export
mapOConst : Functor m => OConst m r x -> OConst m r y
mapOConst omv = OConst_ $ map (mapConst {y}) omv.mv

record Audit v where
  constructor Audit_
  val : v

public export
interface AAt m s where
  AAtInd : Type
  AAtVal : Type

  aAt : Audit AAtInd -> LensLike' m s $ Audit $ Maybe $ Audit AAtVal

public export
AuditSortedMap : Type -> Type -> Type
AuditSortedMap kt vt = Audit $ SortedMap kt (Audit kt, Audit vt)


export
data LensType : (m : Type -> Type) -> Type where
  [noHints]
  ReadLens :    Monad m 
             => LensType (OConst m r)
  WriteLens : Monad m => LensType m

%hint
public export
lensTypeStateTAuditHistm : Monad m => LensType m
lensTypeStateTAuditHistm = WriteLens

%hint
public export
lensTypeOConst : Monad m => LensType (OConst m r)
lensTypeOConst = ReadLens 

aoGet :    Monad m 
        -- => {0 s,a,k : Type} --replace the following line with this, and it compiles and runs fine
        => {s,a,k : Type} 
        -> Audit k
        -> Audit s 
        -> Maybe (Audit a) 
        -> (   aToMA : Audit (Maybe (Audit a)) 
            -> OConst m r (Audit (Maybe (Audit a))))
        -> OConst m r ()
aoGet aK aS resMAA aToMA  = mapOConst $ aToMA $ Audit_ resMAA

    
public export
{k : Type} -> {a : Type} -> {m : Type -> Type} -> LensType m => AAt m (AuditSortedMap k a) where
  AAtInd = k
  AAtVal = a
  aAt @{ReadLens} aK (Mor aToMA) = Mor 
    (\aS => 
       let mAV : Maybe (Audit a) = snd <$> SortedMap.lookup (aK.val) (aS.val)
           res = aoGet aK aS mAV aToMA 
       in mapOConst res
       )
  aAt @{WriteLens} aK (Mor aToMB) = Mor pure
    
public export
MGetting : (m : Type -> Type) -> Functor m => Type -> Type -> Type -> Type
MGetting m r = LensLike' (OConst m r)

public export
mview : Monad m => MGetting m a s a -> s -> m a
mview l =
  let 
      afunc : (a -> OConst m a a) = (\a => OConst_ $ pure (MkConst a))
      (Mor sfunc) = l (Mor afunc)
      --extract the "a" from the const
      resFunc = (\(OConst_ mca) => map (\(MkConst a) => a) mca) . sfunc
  in resFunc
  
main : IO ()
main = let asm : AuditSortedMap Int String = Audit_ SortedMap.empty
           ai : Audit Int = Audit_ 2
       in
         do
           Audit_ v <- mview {m=IO} (aAt {m=OConst IO $ Audit $ Maybe $ Audit String} ai) asm
           
           putStrLn $ maybe "nothing" (.val) v