Hide other unmatchable patterns
Lambdas, in particular. Fixes #1671
commit87897174e5f807d218dd49e603b3c608343bd8f5
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSat 20 Dec 2014, 22:17 (12 years ago)
parent0d8a153
src/Idris/AbsSyntax.hs+3
@@ -1696,6 +1696,9 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
16961696 else PAlternative b alts'
16971697 su (PPair fc p l r) = PPair fc p (su l) (su r)
16981698 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1699+ su t@(PLam _ _ _) = PHidden t
1700+ su t@(PPi _ _ _ _) = PHidden t
1701+ su t@(PEq _ _ _ _ _) = PHidden t
16991702 su t = t
17001703
17011704 ctxt = tt_ctxt i
test/reg055/expected+2
@@ -2,3 +2,5 @@ reg055.idr:5:3:When elaborating left hand side of g:
22Can't match on g ([92mf[0m [91m0[0m)
33reg055.idr:8:3:When elaborating left hand side of h:
44Can't match on h x x
5+reg055a.idr:10:7:When elaborating left hand side of Foo.apply:
6+Can't match on apply (\[95mx[0m => \[95my[0m => [95mx[0m) a
test/reg055/reg055a.idrnew file+12
@@ -0,0 +1,12 @@
1+module Foo
2+
3+-- data CrappySet : (a : Type) -> Ord a -> Type where
4+-- Empty : (inst : Ord a) -> CrappySet a inst
5+-- Item : (inst : Ord a) -> a -> CrappySet a inst -> CrappySet a inst
6+--
7+-- empty : (inst : Ord a) => CrappySet a inst
8+
9+apply : (a -> a -> b) -> a -> a
10+apply (\x => \y => x) a = a
11+apply f a = a
12+
test/reg055/run+3
@@ -1,2 +1,5 @@
11#!/usr/bin/env bash
22idris $@ reg055.idr --check
3+idris $@ reg055a.idr --check
4+rm -f *.ibc
5+