Closed
Conversation
Here we ignore the arity of the constructor and consider only the type to which the constructor belongs. This matches, e.g., both `Zero` and `Succ i`` to a node whose type is `Nat`; whereas the previous implementation, which eta-expands the value constructor's type, would only match `Zero`. Signed-off-by: Drew Hess <src@drewhess.com>
brprice
reviewed
Jun 10, 2023
Comment on lines
588
to
+598
| | Just t <- exprType e -> do | ||
| pure $ | ||
| vcs <&> \vc@(vc', tc, td) -> | ||
| (globalOpt' (t `eqType` valConType tc td vc') (valConName vc'), vc) | ||
| -- Here we ignore the arity of the constructor | ||
| -- and consider only the type to which the | ||
| -- constructor belongs. This matches, e.g., | ||
| -- both @Zero@ and @Succ i@ to a node whose | ||
| -- type is @Nat@; whereas using 'valConType', | ||
| -- which eta-expands the value constructor's | ||
| -- type, would only match @Zero@. | ||
| (globalOpt' (t `eqType` mkTAppCon tc (TVar () . fst <$> astTypeDefParameters td)) (valConName vc'), vc) |
Contributor
There was a problem hiding this comment.
I think we can do better here. (See below)
Background: we only have regular types (i.e. not gadts), so for a type D a b with a constructor C A[a,b], we have that D S T ∋ C A[S,T] (with no restrictions on what S and T (the instantiations of the type's params) are). Thus we only need to check whether the constructor vc is a constructor of D (and that D S T is fully-applied, though this should be guarenteed by the fact that D S T is t in the code, and t = exprType e, thus of kind KType.)
Thus we need to:
- check that
tis of the form "a type constructor applied to a bunch of things" - extract the head
D - check whether
vcis a constructor ofD
I.e. something like (off the top of my head):
Just tc == fmap fst (decomposeTAppCon t)
Contributor
|
Superseded by #1071. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Here we ignore the arity of the constructor and consider only the type to which the constructor belongs. This matches, e.g., both
ZeroandSucc ito a node whose type isNat; whereas the previous implementation, which eta-expands the value constructor's type, would only matchZero.However, the current implementation of this is not quite what we want, because the way I've done this, we've lost the ability to match against any polymorphic type. For example, if we have a hole of type
List Int, we no longer get a match on eitherConsorNil.I've taken this as far as I can for now due to current time constraints, so I'll mark this as a draft for now.