06db7dc · Idris-dev · git.iko.soy

src/Idris/Core/ProofState.hs+2

@@ -566,6 +566,8 @@ solve ctxt env (Bind x (Guess ty val) sc)

566 = do ps <- get

567 dropdots <-

568 case lookup x (notunified ps) of

569+ Just (P _ h _)

570+ | h == x -> return [] -- Can't solve itself!

569 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $

571 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $

570 do match_unify' ctxt env (tm, Just InferredVal)

572 do match_unify' ctxt env (tm, Just InferredVal)

571 (val, Just GivenVal)

573 (val, Just GivenVal)

test/regression002/expected+7

@@ -1,3 +1,10 @@

1+reg001.idr:3:1-9:

2+ |

3+3 | foo a a x = x

4+ | ~~~~~~~~~

5+When checking left hand side of foo:

6+Can't match on foo a a x

7+

1reg003a.idr:4:13-38:

8reg003a.idr:4:13-38:

2 |

9 |

34 | ECons : Nat -> OddList -> EvenList

104 | ECons : Nat -> OddList -> EvenList

test/regression002/run+1

@@ -1,6 +1,7 @@

1#!/usr/bin/env bash

2

3${IDRIS:-idris} $@ --nobanner --nocolour --quiet --port none <<!

4+:load reg001.idr

4:load reg003.idr

5:load reg003.idr

5:load reg003a.idr

6:load reg003a.idr

6:load reg006.idr

7:load reg006.idr