diff --git a/src/Core/Case/Builder.idr b/src/Core/Case/Builder.idr
index f199363..d3c506e 100644
--- a/src/Core/Case/Builder.idr
+++ b/src/Core/Case/Builder.idr
@@ -459,7 +459,7 @@ conTypeEq (CName x tag) (CName x' tag')
              Yes Refl => Just Refl
              No contra => Nothing
 conTypeEq CDelay CDelay = Just Refl
-conTypeEq (CConst x) (CConst y) = cong CConst <$> constantEq x y
+conTypeEq (CConst x) (CConst y) = (\ eq => cong CConst eq) <$> constantEq x y
 conTypeEq _ _ = Nothing
 
 data Group : SnocList Name -> -- variables in scope
diff --git a/src/Core/TT/Name.idr b/src/Core/TT/Name.idr
index 1060f68..c1fe1f4 100644
--- a/src/Core/TT/Name.idr
+++ b/src/Core/TT/Name.idr
@@ -387,7 +387,7 @@ nameEq (NS xs x) (NS ys y) with (decEq xs ys)
     nameEq (NS ys x) (NS ys y) | (Yes Refl) | Nothing = Nothing
     nameEq (NS ys y) (NS ys y) | (Yes Refl) | (Just Refl) = Just Refl
   nameEq (NS xs x) (NS ys y) | (No contra) = Nothing
-nameEq (UN x) (UN y) = map (cong UN) (userNameEq x y)
+nameEq (UN x) (UN y) = map (\ eq => cong UN eq) (userNameEq x y)
 nameEq (MN x t) (MN x' t') with (decEq x x')
   nameEq (MN x t) (MN x t') | (Yes Refl) with (decEq t t')
     nameEq (MN x t) (MN x t) | (Yes Refl) | (Yes Refl) = Just Refl
diff --git a/src/Core/TT/TT.idr b/src/Core/TT/TT.idr
index b2e891f..d46cd21 100644
--- a/src/Core/TT/TT.idr
+++ b/src/Core/TT/TT.idr
@@ -153,7 +153,7 @@ constantEq (Ch x) (Ch y) = case decEq x y of
                                 Yes Refl => Just Refl
                                 No contra => Nothing
 constantEq (Db x) (Db y) = Nothing -- no DecEq for Doubles!
-constantEq (PrT x) (PrT y) = cong PrT <$> primTypeEq x y
+constantEq (PrT x) (PrT y) = (\ eq => cong PrT eq) <$> primTypeEq x y
 constantEq WorldVal WorldVal = Just Refl
 constantEq _ _ = Nothing