The Coq mailing list

[Joachim Breitner <mail AT joachim-breitner.de>]

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/

Attachment: signature.asc
Description: This is a digitally signed message part