Fix corner case with dot patterns
They need to be solvable by unification with another pattern, so it's no
good if the metavariable in the argument position just solves directly
with what the programmer gave.
Fixes #3839
commit06db7dc171686fdc4ea29953d7cdf2ef2ecde1d2
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateTue 9 Jan 2018, 16:53 (9 years ago)
parentd77513b
src/Idris/Core/ProofState.hs+2
@@ -566,6 +566,8 @@ solve ctxt env (Bind x (Guess ty val) sc)
566566 = do ps <- get
567567 dropdots <-
568568 case lookup x (notunified ps) of
569+ Just (P _ h _)
570+ | h == x -> return [] -- Can't solve itself!
569571 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $
570572 do match_unify' ctxt env (tm, Just InferredVal)
571573 (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+
18reg003a.idr:4:13-38:
29 |
3104 | ECons : Nat -> OddList -> EvenList
test/regression002/run+1
@@ -1,6 +1,7 @@
11#!/usr/bin/env bash
22
33${IDRIS:-idris} $@ --nobanner --nocolour --quiet --port none <<!
4+:load reg001.idr
45:load reg003.idr
56:load reg003a.idr
67:load reg006.idr