When I say

{-# LANGUAGE GADTs #-}

data G a where
  GBool :: G Bool

foo GBool = True

I get

    Couldn't match expected type ‘t’ with actual type ‘Bool’
      ‘t’ is untouchable
        inside the constraints (t1 ~ Bool)
        bound by a pattern with constructor
                   GBool :: G Bool,
                 in an equation for ‘foo’
        at /Users/rae/temp/Bug.hs:6:5-9
      ‘t’ is a rigid type variable bound by
          the inferred type of foo :: G t1 -> t at /Users/rae/temp/Bug.hs:6:1
    Relevant bindings include
      foo :: G t1 -> t (bound at /Users/rae/temp/Bug.hs:6:1)
    In the expression: True
    In an equation for ‘foo’: foo GBool = True

My code is indeed bogus and the error message is accurate. But, it's really unhelpful in that the solution to my problem is "add a type signature". In general, I occasionally see folks complain about "untouchable" error messages. Most recently, see this thread, which inspired this report.

Is the solution always to just add a type signature/annotation? Would it make sense to include a link to a stable wiki page about just what "untouchable" variables are? I don't necessarily have a solution to this problem, but I think it's worth thinking about.