Fix for #2535#2542
Conversation
|
It is ready to merge! |
facundominguez
left a comment
There was a problem hiding this comment.
👍 I don't find other things to improve about the code itself, though I left a suggestion for improving documentation.
Probably this should be merged after merging ucsd-progsys/liquid-fixpoint#753 and updating the liquid-fixpoint submodule.
| | length ts == length ts' = RApp c (Misc.zipWithDef go ts $ Bare.matchKindArgs ts ts') p r | ||
| -- Removing length check because Haskell types can contain kinds which is safe based on the comment above | ||
| -- | length ts == length ts' | ||
| = RApp c (Misc.zipWithDef go ts $ Bare.matchKindArgs ts ts') p r |
There was a problem hiding this comment.
This could be a good time to document what goPlug is supposed to do.
There was a problem hiding this comment.
Well, plug is definitely replacing the holes (_) with their actual types, but to do it gets the type information from the GHC types, thus it checks that the two are compatible.
I agree that it would be great to get cleaned/documented, but since this PR fixes an actual bug, I suggest we do it later :)
But I will minimize the fixpoint example!
|
Shall we merge? I simplified the fixpoint example! |
This PR is redoing #2538, which was reverted. @nikivazou, please feel free to work on this branch as needed.