Hide other unmatchable patterns

Lambdas, in particular. Fixes #1671

src/Idris/AbsSyntax.hs

@@ -1696,6 +1696,9 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
                            else PAlternative b alts'
     su (PPair fc p l r) = PPair fc p (su l) (su r)
     su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
+    su t@(PLam _ _ _) = PHidden t
+    su t@(PPi _ _ _ _) = PHidden t
+    su t@(PEq _ _ _ _ _) = PHidden t
     su t = t
 
     ctxt = tt_ctxt i

test/reg055/expected

@@ -2,3 +2,5 @@ reg055.idr:5:3:When elaborating left hand side of g:
 Can't match on  g (f 0)
 reg055.idr:8:3:When elaborating left hand side of h:
 Can't match on  h x x
+reg055a.idr:10:7:When elaborating left hand side of Foo.apply:
+Can't match on  apply (\x => \y => x) a

test/reg055/reg055a.idr

@@ -0,0 +1,12 @@
+module Foo
+
+-- data CrappySet : (a : Type) -> Ord a -> Type where
+--   Empty : (inst : Ord a) -> CrappySet a inst
+--   Item  : (inst : Ord a) -> a -> CrappySet a inst -> CrappySet a inst
+-- 
+-- empty : (inst : Ord a) => CrappySet a inst
+
+apply : (a -> a -> b) -> a -> a
+apply (\x => \y => x) a = a
+apply f a = a 
+

test/reg055/run

@@ -1,2 +1,5 @@
 #!/usr/bin/env bash
 idris $@ reg055.idr --check
+idris $@ reg055a.idr --check
+rm -f *.ibc
+