Type level programming: Dealing with ambiguous type error

AriFordsham:

Having said that, there is a feature of RequiredTypeArguments that I do like. Until now, the only way to go from type (or data kind) -> term was with a typeclass. this has the disadvantage of a) unwieldly syntax (for this use case) and b) It doesn’t support closed classes. By RTA allows me to pattern-match on types in function syntax, which is nice.

Could you give an example of what you mean here? It sounds like you’re saying it’s possible to do something like this:

f :: forall (a :: Type) -> Int
f Int = 0
f Bool = 1

But that gives an error:

• Couldn't match expected type ‘a’ with actual type ‘Int’
  ‘a’ is a rigid type variable bound by
    the type signature for:
      f :: forall a -> Int
• In the pattern: Int
  In an equation for ‘f’: f Int = 0