From 048f1887eadc31dcf32038a94b9ba719415a6aad Mon Sep 17 00:00:00 2001
From: Donovan Crichton <N/A>
Date: Sat, 25 Jul 2020 12:59:33 +1000
Subject: [PATCH] Added explicit case to headEq to allow matching on Pi Types.

---
 src/Core/CaseBuilder.idr | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Core/CaseBuilder.idr b/src/Core/CaseBuilder.idr
index 1db93079f..34bfbf954 100644
--- a/src/Core/CaseBuilder.idr
+++ b/src/Core/CaseBuilder.idr
@@ -601,6 +601,7 @@ sameType {ns} fc phase fn env (p :: xs)
     firstPat (pinf :: _) = pat pinf
 
     headEq : NF ns -> NF ns -> Phase -> Bool
+    headEq (NBind _ _ (Pi _ _ _) _) (NBind _ _ (Pi _ _ _) _) _ = True
     headEq (NTCon _ n _ _ _) (NTCon _ n' _ _ _) _ = n == n'
     headEq (NPrimVal _ c) (NPrimVal _ c') _ = c == c'
     headEq (NType _) (NType _) _ = True