Coverage Checking Loop

[NathanielB123]

Coverage Checking Loop

[andreasabel]

I am hoping @jespercockx will find some time to investigate if there is something to be done about the issue (maybe it is indeed a bug...).

[andreasabel]

Thanks for the report!

Here is a version of the test case without the standard library (and some shortening of identifiers etc.):

interleaved mutual

  record R : Set

  r : R

  data D : R → Set where
    base : D r
    step : D r → D r

  record R where
    inductive; no-eta-equality
    field f : D r

  r = record{ f = base }

foo : ∀ a → D a → Set₁
foo _ base = Set
-- foo _ (step _) = Set  -- without this line, the coverage checker loops

[andreasabel]

So, it seems like there is an infinite loop in the unifier between solving:

1. r =?= r : R (solved by injectivity)
2. base =?= base : D r (solved by injectivity)

Maybe Agda malfunctioning here is not surprising, because this example is very-dependent in the sense that it uses r in types of its own subexpressions (here: base).

@jespercockx : I suppose for base =?= base : D r the unifier somehow also wants to check r =?=r for some reason, am I understanding this correctly?

If my analysis is correct and this is indeed this loop, it could be solved by caching solved unification problems. However, this would then rather be a coinductive unifier for non-well-founded unification problems...

Maybe we need to add a check to Agda instead that rules out the OP, giving an error about illegal dependency?

[NathanielB123]

This is mostly tangentially-related rambling, so feel free to ignore, but I played around with translating the code to Idris2 (given it appears they have similar perhaps-unintentional-and-probably-somewhat-broken support for "very dependent" types - Idris #3129) and both the code snippet above, my original more complicated example typechecked (/failed to typecheck with the appropriate error about foo being non-total) just fine (TreeIntrinsic.idr). Maybe with more effort I could get the typechecker to loop, but as I was writing the code and getting type errors, it seemed at least semi-robust.

If the theory around "very dependent" types genuinely isn't there, then on one hand I guess it makes sense to try and prevent them to keep Agda safe.

However, on the other, afaik (which admittedly is not very far - I am very new to dependent types, so take my opinion with a grain of salt), induction-recursion and induction-induction are also not perfectly well-understood and yet still Agda features them. I don't know how feasible it would be, but I know at least am getting some utility out of being able to define these "very dependent" types, so I would personally like to see better support for them (I suppose behind a flag), rather than them being ruled out with a type error. Of course, assuming the cost of such improved support would not be too great.

[jespercockx]

This looks to me like essentially the same problem as in #1556 (see #1556 (comment)). I remember @andreasabel tried fixing this by using the termination checker on the types of recursive calls, but this caused other problems and was reverted (see #3581, #3662, and #3683). Perhaps it is worth giving it another go.