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

Redefine does not work on default type class methods #142

Open
lastland opened this issue Feb 11, 2020 · 0 comments
Open

Redefine does not work on default type class methods #142

lastland opened this issue Feb 11, 2020 · 0 comments

Comments

@lastland
Copy link
Collaborator

To fix this, one needs to change the following part:

(Nothing, Nothing, Just term) ->
let extraSubst
| meth `elem` classTypes =
let names = foldMap (^..binderIdents) . filter ((== Explicit) . view binderExplicitness)
in M.fromList $ zip (names classArgs) [instTy]
| otherwise =
mempty
in -- In the body of the default definition, make methods names
-- refer to their local version
-- TODO: Associated type defaults should remember that they're types
pure . CM_Defined CL_Term $ subst (allLocalNames <> extraSubst) term

to make it recognize edits.

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

1 participant