Skip to content
This repository has been archived by the owner on Nov 17, 2020. It is now read-only.

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

Closed
nomeata opened this issue Sep 13, 2017 · 1 comment
Closed

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

nomeata opened this issue Sep 13, 2017 · 1 comment

Comments

@nomeata
Copy link
Collaborator

nomeata commented Sep 13, 2017

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
Copy link
Owner

antalsz commented Oct 10, 2017

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

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants