Fix HasExpressions ConstructorApp (#2044)

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>

src/Juvix/Compiler/Internal/Extra.hs

@@ -47,10 +47,18 @@ instance HasExpressions Expression where
     ExpressionHole {} -> f e
 
 instance HasExpressions ConstructorApp where
-  leafExpressions f = traverseOf (constrAppType . _Just) (leafExpressions f)
+  leafExpressions f a = do
+    let _constrAppConstructor = a ^. constrAppConstructor
+    _constrAppType <- traverseOf _Just (leafExpressions f) (a ^. constrAppType)
+    _constrAppParameters <- traverseOf each (leafExpressions f) (a ^. constrAppParameters)
+    pure ConstructorApp {..}
 
 instance HasExpressions PatternArg where
-  leafExpressions f = traverseOf patternArgPattern (leafExpressions f)
+  leafExpressions f a = do
+    let _patternArgIsImplicit = a ^. patternArgIsImplicit
+        _patternArgName = a ^. patternArgName
+    _patternArgPattern <- leafExpressions f (a ^. patternArgPattern)
+    pure PatternArg {..}
 
 instance HasExpressions Pattern where
   leafExpressions f p = case p of
@@ -89,9 +97,10 @@ instance HasExpressions Let where
     pure Let {..}
 
 instance HasExpressions TypedExpression where
-  leafExpressions f t@TypedExpression {..} = do
-    e' <- leafExpressions f _typedExpression
-    pure (t {_typedExpression = e'})
+  leafExpressions f a = do
+    _typedExpression <- leafExpressions f (a ^. typedExpression)
+    _typedType <- leafExpressions f (a ^. typedType)
+    pure TypedExpression {..}
 
 instance HasExpressions SimpleLambda where
   leafExpressions f (SimpleLambda v ty b) = do

test/Typecheck/Positive.hs

@@ -201,7 +201,11 @@ tests =
     posTest
       "Mutual inference inside let"
       $(mkRelDir ".")
-      $(mkRelFile "MutualLet.juvix")
+      $(mkRelFile "MutualLet.juvix"),
+    posTest
+      "Nested pattern match with type variables"
+      $(mkRelDir ".")
+      $(mkRelFile "NestedPatterns.juvix")
   ]
     <> [ compilationTest t | t <- Compilation.tests
        ]

tests/positive/NestedPatterns.juvix

@@ -0,0 +1,15 @@
+module NestedPatterns;
+
+open import Stdlib.Prelude;
+
+type MyList (A : Type) :=
+  | myList : List A -> MyList A;
+
+toList : {A : Type} -> MyList A -> List A;
+toList (myList xs) := xs;
+
+f : MyList Nat -> Nat;
+f xs :=
+  case toList xs
+    | suc n :: nil := n
+    | _ := zero;