Corecords: Inference in type constructor does not work properly.

[sualitu]

The following results in an error when elaborating projection functions:

corecord BisimStream' : Stream' a -> Stream' a -> Type where
  phd : BisimStream' s s' -> (hd s) = (hd s')
  ptl : BisimStream' s s' -> BisimStream' (tl s) (tl s')

Explicitly adding the type to the type constructor solves this:

corecord BisimStream' : (a : Type) -> Stream' a -> Stream' a -> Type where
  phd : BisimStream' a s s' -> (hd s) = (hd s')
  ptl : BisimStream' a s s' -> BisimStream' a (tl s) (tl s')

This problem also exists for records and is as such not a problem with our implementation.

Branch: Corecords

[david-christiansen]

There's a function in the elaborator that adds necessary implicits for unbound variables in a type signature. Do you do something like this?

[sualitu]

Yes I do! I actually call that exact function. The problem is not the inference, but the elaboration of projection functions on the implicit a.

When elaborating left hand side of Test.BisimStream'.implicit_aqty:
Can't unify
        Lazy' LazyCodata
              (BisimStream' aqty (Force (tl aqty s)) (Force (tl aqty s'))) ->
        BisimStream' aqty s s'
with
        BisimStream' p_implicit_aqty (_p_implicit_s) (_p_s')

Specifically:
        Can't unify
                \{uv0} =>
                  Lazy' LazyCodata
                        (BisimStream' aqty
                                      (Force (tl aqty s))
                                      (Force (tl aqty s'))) ->
                  uv
        with
                BisimStream' p_implicit_aqty (_p_implicit_s)

[sualitu]

Just to clarify the above, it happens for all projection functions, not just implicits.

[sualitu]

This fails on the master branch (read: without our changes):

record Foo : Stream a -> Stream a -> Type where
  MkFoo : Foo s s'

 When elaborating left hand side of NoCo.Foo.implicit_a:
     Can't unify
             (s' : Stream a) -> Foo a s s'
     with
             Foo p_implicit_a (_p_implicit_s) (_p_s')

     Specifically:
             Can't unify
                     (s' : Stream a) -> Foo a s s'
             with
                     Foo p_implicit_a (_p_implicit_s) (_p_s')