From 07b7d293a0548f28d313cf620bf3441715429b1f Mon Sep 17 00:00:00 2001 From: Drew Hess Date: Sat, 10 Jun 2023 12:12:25 +0100 Subject: [PATCH] feat: better valcon type matching 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 --- primer/src/Primer/Action/Available.hs | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/primer/src/Primer/Action/Available.hs b/primer/src/Primer/Action/Available.hs index f028a8959..6864e21a1 100644 --- a/primer/src/Primer/Action/Available.hs +++ b/primer/src/Primer/Action/Available.hs @@ -83,6 +83,9 @@ import Primer.Core ( _type, _typeMetaLens, ) +import Primer.Core.Transform ( + mkTAppCon, + ) import Primer.Core.Utils (forgetTypeMetadata, freeVars) import Primer.Def ( ASTDef (..), @@ -104,7 +107,6 @@ import Primer.TypeDef ( TypeDefMap, ValCon (valConArgs), valConName, - valConType, ) import Primer.Typecheck ( Cxt, @@ -586,7 +588,14 @@ options typeDefs defs cxt level def0 sel0 = \case | 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) _ -> pure $ vcs <&> \vc@(vc', _, _) -> (globalOpt . valConName $ vc', vc) exprType e = e ^? _exprMetaLens % _type % _Just % (_chkedAt `afailing` _synthed)