ignore normalization of cases

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs

@@ -131,6 +131,7 @@ queryMetavarFinal h = do
     Just (ExpressionHole h') -> queryMetavarFinal h'
     _ -> return m
 
+-- FIXME the returned expression should have the same location as the original
 strongNormalize' :: forall r. (Members '[ResultBuilder, State InferenceState, NameIdGen] r) => Expression -> Sem r Expression
 strongNormalize' = go
   where
@@ -149,7 +150,7 @@ strongNormalize' = go
       -- We just recurse inside
       ExpressionLet l -> ExpressionLet <$> goLet l
       -- TODO it should normalize like an applied lambda
-      ExpressionCase {} -> error "normalization of case expressions is not supported yet"
+      ExpressionCase c -> return (ExpressionCase c)
 
     goLet :: Let -> Sem r Let
     goLet Let {..} = do

test/Typecheck/Negative.hs

@@ -256,6 +256,13 @@ tests =
       $(mkRelFile "LoopingCoercion.juvix")
       $ \case
         ErrCoercionCycles {} -> Nothing
+        _ -> wrongError,
+    negTest
+      "Wrong type (issue 2771)"
+      $(mkRelDir "issue2771")
+      $(mkRelFile "Main.juvix")
+      $ \case
+        ErrWrongType {} -> Nothing
         _ -> wrongError
   ]
 

tests/positive/issue2771/Main.juvix

@@ -0,0 +1,12 @@
+module Main;
+
+type T := t;
+
+type Box := mkBox { unbox : T };
+
+f (b : Box) : Box :=
+  case b of {
+    mkBox _ := mkBox t
+  };
+
+main : T := f (mkBox t);

tests/positive/issue2771/Package.juvix

@@ -0,0 +1,5 @@
+module Package;
+
+import PackageDescription.V2 open;
+
+package : Package := defaultPackage {name := "issue2771"};