walkie/GameTheory-Idris — pull request #1 by Blaisorblade (2014-02-04 13:37:23+00:00)
Title: Fix typechecking problem

This seems to typecheck. I don't seem to get the concrete syntax of Idris yet, but this worked.
What I'd have written as return type, in fact, is simply `List (for (whoseTurn g {p = p1}) ms)`, but if I type:

```
movesFrom : (g : GameTree Discrete s ms)
-> {default refl p1 : isNode g = True}
-> {default refl p2 : whoseTurn g {p = p1} = i}
-> List (for (whoseTurn g {p = p1}) ms)
movesFrom (Node _ i e) {p2 = refl} = moves e
movesFrom (Leaf _ _) {p2 = refl} impossible
```

I get:
`Game.idr:91:13:No such variable {B127}`

However, if for some reason I try to remove the now redundant param, everything typechecks again:
```
movesFrom : (g : GameTree Discrete s ms)
-> {default refl p1 : isNode g = True}
-> List (for (whoseTurn g {p = p1}) ms)
movesFrom (Node _ i e) = moves e
movesFrom (Leaf _ _) impossible
```

BTW, the manual confirms that the dot patterns are not needed, you just omit the annotations. Though this example would not have needed dot patterns in Agda, since you're not matching on the expression ( `whoseTurn g {p = p1}`) which gets refined by the pattern match (to `i`).