antalsz / hs-to-coq

Convert Haskell source code to Coq source code
https://hs-to-coq.readthedocs.io
MIT License
279 stars 27 forks source link

Unbound variable `a` in `Monoid (Endo a)` instance #9

Closed nomeata closed 7 years ago

nomeata commented 7 years ago

This code (also in examples/test/Endo.v)

module Endo where

import Prelude hiding (Monoid)

class Monoid a where
        mempty  :: a
        mappend :: a -> a -> a
        mconcat :: [a] -> a

newtype Endo a = Endo { appEndo :: a -> a }

instance Monoid (Endo a) where
        mempty = Endo id
        Endo f `mappend` Endo g = Endo (f . g)
        mconcat = foldr Endo.mappend Endo.mempty

produces

Local Definition instance_Monoid__Endo_a__mempty : (Endo a) :=
  Mk_Endo id.

Note how a is not bound!

antalsz commented 7 years ago

Fixed – we forgot to handle this when going post-renamer