My Magic: the Gathering implementation uses a few GADTs. Interestingly they use GADTs in very different ways. Source code is here: https://github.com/MedeaMelana/Magic/blob/master/Magic/src/M...

Let me briefly highlight three of them:

1) Type Question models questions that the game might ask of players. Its constructors are tagged with the type of the answer to that question:

  data Question a where
    AskKeepHand :: Question Bool
    AskTarget   :: [EntityRef] -> Question EntityRef
    ...

This allows me to write cards that ask questions and later on plug in various interpreters of these questions (command line interface, JSON webserver, AI, test framework).

2) The ZoneRef datatype enumerates the various zones in a game of Magic (battlefield, hand, etc) but I've chosen to tag each ZoneRef constructor with a type that indicates what the type of a card is when you look up a reference to a card ("object" in Magic jargon):

  type ObjectRef ty = (ZoneRef ty, Id)
  lookupObject :: ObjectRef ty -> Magic (ObjectOfType ty)

Most functions that take object references as an argument like to constrain the type of the object referenced, and using a GADT allows them to do so. For example, dealing damage to an object (creature or planeswalker):

  data SimpleOneShotEffect = DamageObject Object (ObjectRef TyPermanent) Int ...

3) Type TargetList models zero or more targets a spell on the stack can target. Even though in essence it is just a list of targets, it is a GADT so that it can have a "return type" which is re-evaluated when one of more of the targets change (for example, by a card like Redirect or Reverberate).

Hope this helps!