Cycle detected in solution of metavariable:

[nicolabotta]

I am not sure how to reproduce this in a small, self-contained example but you should be able to download https://gitlab.pik-potsdam.de/botta/Idris2Libs and then do:

idris2 FiniteAsSigmaType/Properties.idr

in the root directory of Idris2Libs. This should work fine. However, doing

idris2 FiniteAsInterface/Properties.idr

should yield

14/16: Building FiniteAsInterface.Finite (FiniteAsInterface/Finite.idr)
15/16: Building FiniteAsInterface.Operations (FiniteAsInterface/Operations.idr)
16/16: Building FiniteAsInterface.Properties (FiniteAsInterface/Properties.idr)
FiniteAsInterface/Properties.idr:24:16--24:35:While processing right hand side of FiniteAsInterface.Properties.toVectComplete at FiniteAsInterface/Properties.idr:23:1--34:1:
While processing type of 2356:s1 at FiniteAsInterface/Properties.idr:24:3--25:3:
Sorry, I can't find any elaboration which works. All errors:
If Fin.Operations.toVect: Cycle detected in solution of metavariable $resolved2372

If FiniteAsInterface.Operations.toVect: Cycle detected in solution of metavariable $resolved2372

Welcome to Idris 2 version 0.0. Enjoy yourself!
FiniteAsInterface.Properties>

This is strange because the type of s1 in FiniteAsInterface.Properties.toVectComplete is the same as the type of s1 in FiniteAsSigmaType.Properties.toVectComplete.

If you think it's worth, I can try to build a self-contained example of this behavior.

[nicolabotta]

Here is a self-contained example:

module issues.FiniteAsInterface

import Data.Fin
import Data.Vect

tail : {0 A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail f = f . FS

toVect : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVect {n =   Z} _ = Nil
toVect {n = S m} f = (f FZ) :: (toVect (tail f))

record Iso a b where
  constructor MkIso
  to : a -> b
  from : b -> a
  toFrom : (y : b) -> to (from y) = y
  fromTo : (x : a) -> from (to x) = x

---

interface Finite t where
  card : Nat
  iso  : Iso t (Fin card)  

foo : (Finite t) => Vect (card {t}) t
foo = toVect (from iso)

toVectComplete : (Finite t) => (x : t) -> Elem x foo
toVectComplete a = s3 where
  s1  :  Elem (from iso (to iso a)) (toVect (from iso))
  s1  =  ?s1def
  s2  :  from iso (to iso a) = a
  s2  =  fromTo iso a
  s3  :  Elem a (toVect (from iso))
  s3  =  replace {p = \ z => Elem z (toVect (from iso))} s2 s1

The error is the same:

nicola@lt561:~/gitlab/botta/Idris2Libs$ idris2 issues/FiniteAsInterface.idr 
1/1: Building issues.FiniteAsInterface (issues/FiniteAsInterface.idr)
issues/FiniteAsInterface.idr:31:16--31:35:While processing right hand side of issues.FiniteAsInterface.toVectComplete at issues/FiniteAsInterface.idr:30:1--41:1:
While processing type of 2142:s1 at issues/FiniteAsInterface.idr:31:3--32:3:
Cycle detected in solution of metavariable $resolved2167
Welcome to Idris 2 version 0.0. Enjoy yourself!
issues.FiniteAsInterface>

[edwinb]

I'll take a closer look. At best, this is a bad error message because it hasn't said what the internal name refers to, and because it hasn't said what the cyclic definition is. This message should indicate a problem with the program, but it's the first time I've seen it other than in contrived circumstances so I'll need to have a proper look first.

[edwinb]

I don't know if this will help me be organised, but I've added a label that I hope will remind me to investigate!