From 8cee46f7c988699253d350d7ede000e9f889f4f4 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 22 Sep 2023 19:40:49 +0200
Subject: [PATCH] support functions in instance parameters

---
 .../Compiler/Internal/Data/InstanceInfo.hs    | 27 ++++++++++++++++++-
 .../Analysis/TypeChecking/Traits/Resolver.hs  |  5 ++++
 tests/Compilation/positive/out/test061.out    |  1 +
 tests/Compilation/positive/test061.juvix      | 13 ++++++++-
 4 files changed, 44 insertions(+), 2 deletions(-)

diff --git a/src/Juvix/Compiler/Internal/Data/InstanceInfo.hs b/src/Juvix/Compiler/Internal/Data/InstanceInfo.hs
index b8af4336d4..4e9e73fcac 100644
--- a/src/Juvix/Compiler/Internal/Data/InstanceInfo.hs
+++ b/src/Juvix/Compiler/Internal/Data/InstanceInfo.hs
@@ -9,6 +9,7 @@ import Juvix.Prelude
 data InstanceParam
   = InstanceParamVar VarName
   | InstanceParamApp InstanceApp
+  | InstanceParamFun InstanceFun
   | InstanceParamHole Hole
   | InstanceParamMeta VarName
   deriving stock (Eq)
@@ -21,6 +22,14 @@ data InstanceApp = InstanceApp
   }
   deriving stock (Eq)
 
+data InstanceFun = InstanceFun
+  { _instanceFunLeft :: InstanceParam,
+    _instanceFunRight :: InstanceParam,
+    -- | The original expression from which this InstanceFun was created
+    _instanceFunExpression :: Expression
+  }
+  deriving stock (Eq)
+
 data InstanceInfo = InstanceInfo
   { _instanceInfoInductive :: InductiveName,
     _instanceInfoParams :: [InstanceParam],
@@ -38,6 +47,7 @@ newtype InstanceTable = InstanceTable
   }
 
 makeLenses ''InstanceApp
+makeLenses ''InstanceFun
 makeLenses ''InstanceInfo
 makeLenses ''InstanceTable
 
@@ -68,8 +78,10 @@ paramToExpression :: InstanceParam -> Expression
 paramToExpression = \case
   InstanceParamVar v ->
     ExpressionIden (IdenVar v)
-  InstanceParamApp (InstanceApp {..}) ->
+  InstanceParamApp InstanceApp {..} ->
     _instanceAppExpression
+  InstanceParamFun InstanceFun {..} ->
+    _instanceFunExpression
   InstanceParamHole h -> ExpressionHole h
   InstanceParamMeta {} ->
     impossible
@@ -118,6 +130,17 @@ paramFromExpression metaVars e = case e of
               }
       _ ->
         Nothing
+  ExpressionFunction Function {..}
+    | _functionLeft ^. paramImplicit == Explicit -> do
+        l <- paramFromExpression metaVars (_functionLeft ^. paramType)
+        r <- paramFromExpression metaVars _functionRight
+        return $
+          InstanceParamFun
+            InstanceFun
+              { _instanceFunLeft = l,
+                _instanceFunRight = r,
+                _instanceFunExpression = e
+              }
   _ ->
     Nothing
 
@@ -146,3 +169,5 @@ checkNoMeta = \case
   InstanceParamMeta {} -> False
   InstanceParamHole {} -> True
   InstanceParamApp InstanceApp {..} -> all checkNoMeta _instanceAppArgs
+  InstanceParamFun InstanceFun {..} ->
+    checkNoMeta _instanceFunLeft && checkNoMeta _instanceFunRight
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs
index d3522cb068..ef6334fb4c 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs
@@ -129,8 +129,13 @@ lookupInstance' canFillHoles tab name params = do
       (InstanceParamApp app1, InstanceParamApp app2)
         | app1 ^. instanceAppHead == app2 ^. instanceAppHead -> do
             and <$> sequence (zipWithExact goMatch (app1 ^. instanceAppArgs) (app2 ^. instanceAppArgs))
+      (InstanceParamFun fun1, InstanceParamFun fun2) -> do
+        l <- goMatch (fun1 ^. instanceFunLeft) (fun2 ^. instanceFunLeft)
+        r <- goMatch (fun1 ^. instanceFunRight) (fun2 ^. instanceFunRight)
+        return $ l && r
       (InstanceParamVar {}, _) -> return False
       (InstanceParamApp {}, _) -> return False
+      (InstanceParamFun {}, _) -> return False
 
 lookupInstance ::
   forall r.
diff --git a/tests/Compilation/positive/out/test061.out b/tests/Compilation/positive/out/test061.out
index 01961e4c34..aa0dd1ce80 100644
--- a/tests/Compilation/positive/out/test061.out
+++ b/tests/Compilation/positive/out/test061.out
@@ -12,3 +12,4 @@ abba
 abba!
 abba3
 a :: b :: c :: d :: nil
+\{ true := false | false := true }
diff --git a/tests/Compilation/positive/test061.juvix b/tests/Compilation/positive/test061.juvix
index 84e37d3b5c..e7ca759157 100644
--- a/tests/Compilation/positive/test061.juvix
+++ b/tests/Compilation/positive/test061.juvix
@@ -49,6 +49,16 @@ f'4 {A} {{_ : Show A}} : A → String := Show.show;
 
 f5 {A} {{Show A}} (n : String) (a : A) : String := n ++str Show.show a;
 
+showBoolFun (f : Bool → Bool) : String :=
+  let
+    b1 : Bool := f true;
+    b2 : Bool := f false;
+  in
+  "\\{ true := " ++str Show.show b1 ++str " | false := " ++str Show.show b2 ++str " }";
+
+instance
+showBoolFunI : Show (Bool → Bool) := mkShow (show := showBoolFun);
+
 main : IO :=
   printStringLn (Show.show true) >>
   printStringLn (f false) >>
@@ -63,4 +73,5 @@ main : IO :=
   printStringLn (f'3 "abba") >>
   printStringLn (f'3 {{M := mkShow (λ{x := x ++str "!"})}} "abba") >>
   printStringLn (f5 "abba" 3) >>
-  printStringLn (Show.show ["a"; "b"; "c"; "d"]);
+  printStringLn (Show.show ["a"; "b"; "c"; "d"]) >>
+  printStringLn (Show.show (λ{x := not x}));