[ufo]

What an interesting example. Not what I was expecting!

Can you think of an example of a bug that you avoided due to the extra type safety of gadts? Magic has some pretty complex rules so I imagine that writing exaustive test must be hard and that the extra static guarantees might be able to find something a dynamic checker wouldn't. (Its ok if you need some ingame jargon to explain that, I know the basic rules).

[Martijn]

It's a combination of avoiding potential bugs and just modelling things differently altogether:

If I had to leave out the answer type of questions, I'd have to come up with an entirely different way of modelling answers. For example, I might have had to write a datatype like:

  data Answer = AnswerBool Bool | AnswerInt Int | ...

and then processing the answer (through pattern matching) would have to discard any answer it didn't like, which is awkward. Or I would have had to use a type class to keep everything type-safe which would have resulted in more complicated type signatures throughout the code.

For the TargetList, the current setup allows me to write functions that consume a target list of exactly the right size, for example:

  \(target1, target2) -> ...

rather than a normal list:

  \[target1, target2] -> ...

which in this case results in a pattern match exception if you pass it a list of any length other than 2.