The Coq mailing list

[Merlin Göttlinger <megoettlinger AT gmail.com>]

Hi,

after rewriting all my typeclasses to this CPS-transformed ones, it was still one indirection too many for the termination checker BUT if I additionally change traverse to sequence after Vector.map it works as expected. It is also entirely possible that I made a mistake somewhere that causes this behaviour but at any rate it works now without having to inline the vector definition or other tricks.

Thanks for your help.

Cheers,

Merlin

Joachim Breitner <mail AT joachim-breitner.de> schrieb am Fr., 5. Jan. 2018 um 21:37 Uhr:

Hi,

I at least found the time to search for where I wrote about this
before. I think you are hitting the problem that I describe in
https://stackoverflow.com/q/47082796/946226
The question talks about records, and not classes, but since Coq
classes are (normally) record type, it is the same problem – the
termination checker runs after type class resolution and sees the
underlying record.

I describe our solution with CPS-transformed types for classes in the
first answer.

Feel free to ask for further clarification, either here or on SE.

Cheers,
Joachim


Am Freitag, den 05.01.2018, 18:55 +0000 schrieb Merlin Göttlinger:
> Hi,
>
> that sounds promising. I would be interrested to hear how this trick works because it certainly isn't obvious to me from looking a tthe code.
> So if you find the time later on to explain this I would be greatfull, but in any case thank you both for your help.
>
> Cheers,
> Merlin
>
> Joachim Breitner <mail AT joachim-breitner.de> schrieb am Fr., 5. Jan. 2018 um 19:14 Uhr:
> > Hi,
> >
> > Am Freitag, den 05.01.2018, 11:54 +0000 schrieb Merlin Göttlinger:
> > > VectorUtils.traverse depends on a bunch of stuff I implemented and is
> > > the usual operation known from e.g. Haskell with signature G A -> (A
> > > -> F B) -> F (G B) where G is (fun T => Vector.t T n) and F is list
> > > in my case.
> >
> > Coq’s termination checker cannot look through type class instances.
> >
> > There is a trick, however, if you get to choose the type class. See
> > https://github.com/antalsz/hs-to-coq/blob/master/base/GHC/Base.v#L41-L54
> > and let me know if you want more explanation (I am on the run right
> > now).
> >
> > Joachim
> >
> > --
> > Joachim Breitner
> >   mail AT joachim-breitner.de
> >   http://www.joachim-breitner.de/
--
Joachim Breitner
  mail AT joachim-breitner.de
  http://www.joachim-breitner.de/