CaseOfCase kind mismatch error fix (IntersectMBO#5923)

* Fix issue IntersectMBO#5922

* test_extractTyArgs

* CaseOfCase: cover types with two type args

plutus-core/plutus-core.cabal

@@ -608,6 +608,7 @@ test-suite plutus-ir-test
     PlutusIR.Compiler.Error.Tests
     PlutusIR.Compiler.Let.Tests
     PlutusIR.Compiler.Recursion.Tests
+    PlutusIR.Contexts.Tests
     PlutusIR.Core.Tests
     PlutusIR.Generators.QuickCheck.Tests
     PlutusIR.Parser.Tests

plutus-core/plutus-ir/src/PlutusIR/Contexts.hs

@@ -8,6 +8,7 @@
 module PlutusIR.Contexts where
 
 import Control.Lens
+import Data.DList qualified as DList
 import Data.Functor (void)
 import PlutusCore.Arity
 import PlutusCore.Name.Unique qualified as PLC
@@ -132,11 +133,16 @@ data SplitMatchContext tyname name uni fun a = SplitMatchContext
   , smBranches  :: AppContext tyname name uni fun a
   }
 
+-- | Extract the type application arguments from an 'AppContext'.
+-- Returns 'Nothing' if the context contains a TermAppContext.
+-- See 'test_extractTyArgs'
 extractTyArgs :: AppContext tyname name uni fun a -> Maybe [Type tyname uni a]
-extractTyArgs = go []
-  where go acc (TypeAppContext ty _ ctx) = go (ty:acc) ctx
-        go _ (TermAppContext{})          = Nothing
-        go acc AppContextEnd             = Just acc
+extractTyArgs = go DList.empty
+  where
+    go acc = \case
+      TypeAppContext ty _ann ctx -> go (DList.snoc acc ty) ctx
+      TermAppContext{}           -> Nothing
+      AppContextEnd              -> Just (DList.toList acc)
 
 -- | Split a normal datatype 'match'.
 splitNormalDatatypeMatch

plutus-core/plutus-ir/test/PlutusIR/Contexts/Tests.hs

@@ -0,0 +1,40 @@
+{-# LANGUAGE BlockArguments    #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module PlutusIR.Contexts.Tests where
+
+import PlutusIR
+import PlutusIR.Contexts
+
+import PlutusCore.Default (DefaultFun, DefaultUni)
+import PlutusCore.Name.Unique (Unique (..))
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (testCase, (@?=))
+
+test_extractTyArgs :: TestTree
+test_extractTyArgs =
+  testGroup
+    "Applying extractTyArgs to an"
+    [ testCase "empty AppContext evaluates to an empty list of ty args" do
+        extractTyArgs AppContextEnd @?= Just ([] :: [Type TyName DefaultUni ()])
+    , testCase "AppContext without type applications evaluates to Nothing" do
+        extractTyArgs (TermAppContext term () AppContextEnd) @?= Nothing
+    , testCase "AppContext with a mix of term and type applications evaluates to Nothing" do
+        extractTyArgs (TypeAppContext ty1 () (TermAppContext term () AppContextEnd)) @?= Nothing
+        extractTyArgs (TermAppContext term () (TypeAppContext ty1 () AppContextEnd)) @?= Nothing
+    , testCase "AppContext with type applications only evaluates to Just (list of ty vars)" do
+        extractTyArgs (TypeAppContext ty1 () (TypeAppContext ty2 () AppContextEnd))
+          @?= Just [ty1, ty2]
+    ]
+
+----------------------------------------------------------------------------------------------------
+-- Test values -------------------------------------------------------------------------------------
+
+term :: Term TyName Name DefaultUni DefaultFun ()
+term = Var () (Name "x" (Unique 0))
+
+ty1 :: Type TyName DefaultUni ()
+ty1 = TyVar () (TyName (Name "t" (Unique 0)))
+
+ty2 :: Type TyName DefaultUni ()
+ty2 = TyVar () (TyName (Name "t" (Unique 1)))

plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/Tests.hs

@@ -21,6 +21,7 @@ test_caseOfCase = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"]
             , "builtinBool"
             , "largeExpr"
             , "exponential"
+            , "twoTyArgs"
             ]
 
 prop_caseOfCase :: Property

plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/twoTyArgs

@@ -0,0 +1,30 @@
+(let
+  (nonrec)
+  (datatypebind
+    (datatype
+      (tyvardecl d12 (fun (fun (type) (type)) (fun (type) (type))))
+      (tyvardecl a3 (fun (type) (type))) (tyvardecl a10 (type))
+      m11
+      (vardecl c6 (fun (con unit) [ [ d12 a3 ] a10 ]))
+    )
+  )
+  [
+    {
+      [
+        { { m11 (con list) } (con unit) }
+        [
+          {
+            [
+              { { m11 (con list) } (con unit) }
+              (error [ [ d12 (con list) ] (con unit) ])
+            ]
+            [ [ d12 (con list) ] (con unit) ]
+          }
+          (lam x23 (con unit) (error [ [ d12 (con list) ] (con unit) ]))
+        ]
+      ]
+      (con unit)
+    }
+    (error (fun (con unit) (con unit)))
+  ]
+)

plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/twoTyArgs.golden

@@ -0,0 +1,40 @@
+(let
+  (nonrec)
+  (datatypebind
+    (datatype
+      (tyvardecl d12 (fun (fun (type) (type)) (fun (type) (type))))
+      (tyvardecl a3 (fun (type) (type))) (tyvardecl a10 (type))
+      m11
+      (vardecl c6 (fun (con unit) [ [ d12 a3 ] a10 ]))
+    )
+  )
+  (let
+    (nonrec)
+    (termbind
+      (strict)
+      (vardecl k_caseOfCase (fun [ [ d12 (con list) ] (con unit) ] (con unit)))
+      (lam
+        scrutinee
+        [ [ d12 (con list) ] (con unit) ]
+        [
+          { [ { { m11 (con list) } (con unit) } scrutinee ] (con unit) }
+          (error (fun (con unit) (con unit)))
+        ]
+      )
+    )
+    [
+      {
+        [
+          { { m11 (con list) } (con unit) }
+          (error [ [ d12 (con list) ] (con unit) ])
+        ]
+        (con unit)
+      }
+      (lam
+        x23
+        (con unit)
+        [ k_caseOfCase (error [ [ d12 (con list) ] (con unit) ]) ]
+      )
+    ]
+  )
+)