idris-lang/Idris-dev — pull request #1510 by soimort (2014-09-03 16:55:21+00:00)
Title: Support uniqueness types when executing IO actions in REPL

This PR is a follow-up on #1478.

I was playing around with some low-level system binding stuff (with IO). Everything type-checks and compiles perfectly, but REPL complains about a missing pattern:

```
> :t ls
Ish.ls : List Option -> List String -> List String

> :x ls [] ["foo"]
src/Idris/Core/Execute.hs:(163,1)-(207,44): Non-exhaustive patterns in function doExec
```

Adding `EUType` for uniqueness types fixes this problem in REPL.