Fix typechecking problem

This seems to typecheck. I don't seem to get the concrete syntax of Idris yet, but this worked.

### Possible alternatives

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}`
The position points to the type signature.

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
```

So, I just don't get the Idris diagnostic. Maybe it doesn't like me to pass twice the same thing. Or maybe `i` somehow does not get bound in the non-working signature (which seems most reasonable), because it's only used once.

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`).