Support deriving via #3824
Support deriving via #3824
Conversation
|
|
Oh thank you, I added the guilty case 🙇 Also I fixed my error messages and moved most of the deriving via checks into the type checker because I was duplicating a lot of work to infer kinds. |
| @@ -123,6 +123,7 @@ import Language.PureScript.PSString (PSString) | |||
| 'then' { SourceToken _ (TokLowerName [] "then") } | |||
| 'true' { SourceToken _ (TokLowerName [] "true") } | |||
| 'type' { SourceToken _ (TokLowerName [] "type") } | |||
| 'via' { SourceToken _ (TokLowerName [] "via") } | |||
There was a problem hiding this comment.
Since this is a contextual keyword, you will need to make sure to add it ident, qualIdent, and label.
There was a problem hiding this comment.
Good catch! Sorry about that, I added a few test cases to cover this.
|
I managed to ensure the via kind unifies with the kind of the type for which the instance is derived! Elaborating the kinds didn’t work but inferring them after binding all free variables to fresh kinds (like it is done when checking instances declarations) does 🎉 |
kl0tl
force-pushed
the
deriving-via
branch
2 times, most recently
from
2a3abeb
to
25050ef
Compare
| , solverDeferErrors = False | ||
| } | ||
| void . flip runStateT M.empty . runWriterT $ | ||
| entails solverOptions constraint M.empty [] |
There was a problem hiding this comment.
Does this throw away the unsolved constraints?
There was a problem hiding this comment.
Oh, but that's fine because of the current SolverOptions, so the solver won't emit unsolved constraints and instead just fail, right? I guess that means we can't write something like
data T
derive via (...) instance blah :: Coercible X Y => Cls Ti.e. defer Coercible constraints in the instance head, but that's not a big loss, and maybe something that can be solved later?
There was a problem hiding this comment.
The solver indeed fails when typechecking the instance declaration if the generated constraint can’t be solved but it doesn’t try to solve the instance context, so you can write such instance.
| gSimple (MissingNewtypeSuperclassInstance cl1 cl2 ts) = MissingNewtypeSuperclassInstance cl1 cl2 <$> traverse f ts | ||
| gSimple (UnverifiableSuperclassInstance cl1 cl2 ts) = UnverifiableSuperclassInstance cl1 cl2 <$> traverse f ts | ||
| gSimple (InvalidViaType cl ts viaTy) = InvalidViaType cl <$> traverse f ts <*> f viaTy | ||
| gSimple (InvalidViaKind cl ts viaTy viaKind expectedKind) = InvalidViaKind cl <$> traverse f ts <*> f viaTy <*> f viaKind <*> f expectedKind |
There was a problem hiding this comment.
Should f be called on kinds here? There’s no case for the KindsDoNotUnify error for instance so maybe it shouldn’t 🤔
There was a problem hiding this comment.
If there are cases that are missing it's probably an oversight.
There was a problem hiding this comment.
The following SimpleErrorMessage constructors hold SourceTypes but aren’t matched:
InfiniteKindEscapedSkolemKindsDoNotUnifyMissingClassMemberUserDefinedWarningQuantificationCheckFailureInTypeUnsupportedTypeInKind
Should I add cases for them in this PR? Matching every constructor explicitly would be verbose but could help to prevent this in the future.
|
One thing to consider with this syntax is #1120. If we allowed |
It looks like it works but there’s a few things I need help with:
ParensInTypein various places. This constructor doesn’t usually seem to be present in types but it is in via types. Is it supposed to be somehow removed?NoInstanceFoundwhen the kinds of the via type and of the instance head last type don’t unify. I tried to elaborate those kinds but elaborating the kind of an application whose first parameter has a polymorphic kind fails.For instance
Data.Functor.Compose.Composehas such a polymorphic kind:meaning that elaborating the kind of
Compose (Either e) Maybefails when elaborating the application ofComposetoEither e. Should I approach this differently?Also I took the liberty to rename
MissingNewtypeSuperclassInstancetoMissingSuperclassInstancesince this error is thrown for both newtype and via instances, removed the mention of derived superclass instance from its message (since any instance actually qualify) and replaced theInvalidNewtypeInstanceerror thrown when trying to derive a newtype instance for a nullary type class by a newCannotDeriveNullaryTypeClassInstanceerror (which is also thrown for via instances).Close #3302.