On Thu, May 4, 2017 at 10:20 AM, Wolfgang Jeltsch
Today I encountered for the first time the notion of an “untouchable” type variable. I have no clue what this is supposed to mean.
Fwiw, "untouchable" variables come from existential quantification (since the variable must be held abstract so that it doesn't escape). More often we see these errors when using GADTs and TypeFamilies, since both of those often have existentials hiding under the hood in how they deal with indices.
A minimal example that exposes my problem is the following:
{-# LANGUAGE Rank2Types, TypeFamilies #-}
import GHC.Exts (Constraint)
type family F a b :: Constraint
data T b c = T
f :: (forall b . F a b => T b c) -> a f _ = undefined
FWIW, the error comes specifically from the fact that @F@ is a family. If you use a plain old type class, or if you use a type alias (via -XConstraintKinds) then it typechecks just fine. So it's something about how the arguments to @F@ are indices rather than parameters. I have a few guesses about why the families don't work here, but I'm not finding any of them particularly convincing. Really, imo, @c@ should be held abstract within the type of the argument, since it's universally quantified from outside. Whatever @F a b@ evaluates to can't possibly have an impact on @c@[1]. I'd file a bug report. If it's just an implementation defect, then the GHC devs will want to know. And if there's actually a type theoretic reason I missed, it'd be good to have that documented somewhere. [1] For three reasons combined: (1) @F a b@ can't see @c@, so the only effect evaluating @F a b@ could possibly have on @c@ is to communicate via some side channel, of which I only see two: (2) the @(a,c)@ from outside are quantified parametrically, thus nothing from the outside scope could cause information to flow from @a@ to @c@, (3) the @T@ is parametric in @(b,c)@ (since it is not a GADT) so it can't cause information to flow from @b@ to @c@. -- Live well, ~wren