Untouchable type variables

[Dan Doel]

This doesn't sound like the right explanation to me. Untouchable variables
don't have anything (necessarily) to do with existential quantification.
What they have to do with is GHC's (equality) constraint solving.

I don't completely understand the algorithm. However, from what I've read
and seen of the way it works, I can tell you why you might see the error
reported here....

When type checking moves under a 'fancy' context, all (not sure if it's
actually all) variables made outside that context are rendered untouchable,
and are not able to be unified with local variables inside the context. So
the problem that is occurring is related to `c` being bound outside the
'fancy' context `F a b`, but used inside (and maybe not appearing in the
fancy context is a factor). And `F a b` is fancy because GHC just has to
assume the worst about type families (that don't reduce, anyway). Equality
constraints are the fundamental 'fancy' context, I think.

The more precise explanation is, of course, in the paper describing the
current type checking algorithm. I don't recall the motivation, but they do
have one. :) Maybe it's overly aggressive, but I really can't say myself.

-- Dan


On Sun, Jun 18, 2017 at 3:02 PM, wren romano <winterkoninkje at gmail.com>
wrote:

> On Thu, May 4, 2017 at 10:20 AM, Wolfgang Jeltsch
> <g9ks157k at acme.softbase.org> wrote:
> > 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 at .
>
> --
> Live well,
> ~wren
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20170619/f0903ed2/attachment.html>