Case analysis on types in corecords leads to a unification error

[tdidriksen]

Trying to define the following program:

corecord Gedde : Type where
  han : Gedde -> Maybe Nat
  hun : Gedde -> (n : Nat) -> fisk Nat (Just n)
  stime : Gedde -> Gedde
  uvist : (john : Gedde) -> case han john of
                              Just n => Vect n (Maybe Nat)
                              Nothing => Bool

I get the error:

When elaborating right hand side of x.Gedde.uvist:
Can't unify
        case block in MkGedde han hun stime han
with
        case block in MkGedde han
                              hun
                              (Delay (Force (Delay (Force stime))))
                              han

Specifically:
        Can't unify
                case block in MkGedde han hun stime han
        with
                case block in MkGedde han
                                      hun
                                      (Delay (Force (Delay (Force stime))))
                                      han

However, an equivalent record definition only issues warnings:

record A : Type where
  MkA : (han : Maybe Nat) -> (hun : (n : Nat) -> 
            fisk Nat (Just n)) -> (stime : A) -> 
            (uvist : case han of
                           Just n => Vect n (Maybe Nat)
                           Nothing => Bool) -> 
            A

I believe case analysis in types in corecords should be possible.

[sualitu]

The bug occurs when elaborating the projection function.

Interestingly this works:

corecord Alpha : Type where
  bravo : Alpha -> Bool
  charlie : (a : Alpha) -> case (bravo a) of
                             True => Alpha
                             False => Nat

The problem seem to arise from having case analysis in one projection and having another earlier defined projection being recursively defined.