8789717 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+3

@@ -1696,6 +1696,9 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

1696 else PAlternative b alts'

1697 su (PPair fc p l r) = PPair fc p (su l) (su r)

1698 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

1699 su t = t

1702 su t = t

1700

1703

1701 ctxt = tt_ctxt i

1704 ctxt = tt_ctxt i

test/reg055/expected+2

@@ -2,3 +2,5 @@ reg055.idr:5:3:When elaborating left hand side of g:

2Can't match on g ([92mf[0m [91m0[0m)

3reg055.idr:8:3:When elaborating left hand side of h:

4Can'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 @@

1#!/usr/bin/env bash

2idris $@ reg055.idr --check

3+idris $@ reg055a.idr --check

4+rm -f *.ibc

5+