From 3728ba88e20c9cfcf063fc6a5b60f10798008076 Mon Sep 17 00:00:00 2001
From: Aleksei Volkov <volkov.aa@phystech.edu>
Date: Mon, 27 Nov 2023 22:37:39 +0300
Subject: [PATCH] [ fix ] handling of `VCase` in `Core.Case.Builder.sameType`

Current implementation of `headEq` inside `Core.Case.Builder.sameType`
considers two `VCase`s to always be different. Because of this, the
following example fails to compile.

```idris
module Main

public export
record X (flag : Bool) where
  constructor MkX
  x : if flag then Bool else Void

f : X True -> ()
f (MkX True) = ()
f (MkX False) = ()
```

Instead, the following compilation error is produced:

```
Error: Patterns for f require matching on different types.

Main:13:1--13:18
 09 |   constructor MkX
 10 |   x : if flag then Bool else Void
 11 |
 12 | f : X True -> ()
 13 | f (MkX True) = ()
      ^^^^^^^^^^^^^^^^^
```

This patch changes the behaviour of `headEq` to make it treat `VCase`s
as equal, eliminating the error.
---
 src/Core/Case/Builder.idr | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Core/Case/Builder.idr b/src/Core/Case/Builder.idr
index d3c506e9..717d320a 100644
--- a/src/Core/Case/Builder.idr
+++ b/src/Core/Case/Builder.idr
@@ -836,6 +836,7 @@ sameType {ns} fc phase fn env (p :: xs)
     headEq : NF ns -> NF ns -> Phase -> Bool
     headEq (VBind _ _ (Pi _ _ _ _) _) (VBind _ _ (Pi _ _ _ _) _) _ = True
     headEq (VTCon _ n _ _) (VTCon _ n' _ _) _ = n == n'
+    headEq (VCase _ _ _ _ _ _) (VCase _ _ _ _ _ _) _ = True
     headEq (VPrimVal _ c) (VPrimVal _ c') _ = c == c'
     headEq (VType _ _) (VType _ _) _ = True
     headEq (VApp _ _ n _ _) (VApp _ _ n' _ _) RunTime = n == n'