Mimer internal error when querying `recRecursive`

[andreasabel]

Mimer internal error when querying `recRecursive`

[UlfNorell]

We hit the impossible because recMutual is Nothing for Relation.Binary.Bundles.Setoid. The docs say it should only be Nothing if it hasn't yet been computed by the positivity checker, so not sure what's going on here.

Here's a self-contained test case:

module _ where

open import Agda.Primitive

record Point (A : Set) : Set where
  field
    pt : A

record PointedSet : Set₁ where
  field
    Carrier : Set
    point   : Point Carrier

module _ (sto : PointedSet) where

  foo : Set
  foo = {!!}