Untouchable type variables

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Untouchable type variables

Wolfgang Jeltsch-2
Hi!

Today I encountered for the first time the notion of an “untouchable”
type variable. I have no clue what this is supposed to mean. 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

This results in the following error message from GHC 8.0.1:

> Untouchable.hs:9:6: error:
>     • Couldn't match type ‘c0’ with ‘c’
>         ‘c0’ is untouchable
>           inside the constraints: F a b
>           bound by the type signature for:
>                      f :: F a b => T b c0
>           at Untouchable.hs:9:6-37
>       ‘c’ is a rigid type variable bound by
>         the type signature for:
>           f :: forall a c. (forall b. F a b => T b c) -> a
>         at Untouchable.hs:9:6
>       Expected type: T b c0
>         Actual type: T b c
>     • In the ambiguity check for ‘f’
>       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
>       In the type signature:
>         f :: (forall b. F a b => T b c) -> a

I have no idea what the problem is. The type of f looks fine to me. The
type variable c should be universally quantified at the outermost level.
Why does the type checker even introduce a type variable c0?

All the best,
Wolfgang
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Untouchable type variables

wren romano
On Thu, May 4, 2017 at 10:20 AM, Wolfgang Jeltsch
<[hidden email]> 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@.

--
Live well,
~wren
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Untouchable type variables

Wolfgang Jeltsch-2
Am Sonntag, den 18.06.2017, 12:02 -0700 schrieb wren romano:

> > > {-# 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@. 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.

I already filed a bug report:

    https://ghc.haskell.org/trac/ghc/ticket/13655

In a comment, Simon says that this behavior is according to the rules. I
am just not sure whether the rules have to be as they are.

All the best,
Wolfgang
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Untouchable type variables

Dan Doel
In reply to this post by wren romano
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 <[hidden email]> wrote:
On Thu, May 4, 2017 at 10:20 AM, Wolfgang Jeltsch
<[hidden email]> 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@.

--
Live well,
~wren
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Untouchable type variables

Clinton Mead
I'm no expert on type deduction, but it seems to me that GHC rejecting this is perfectly reasonable.

Indeed GHC happy compiles it if you add an instance which can reduce like so:

> type instance F a b = ()

But without that instance, that function is never callable. There could be a whole raft of instances like:

>  type instance F a Int = ...
>  type instance F a Double = ...

etc. As F is open, it must always assume that there could be more instances added, any of which could make the function never callable. So it has to assumes it can never be called. Hence it throws an error, which we can quieten with ambiguous types, but even then "f" is not callable. 

On Mon, Jun 19, 2017 at 2:45 PM, Dan Doel <[hidden email]> wrote:
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 <[hidden email]> wrote:
On Thu, May 4, 2017 at 10:20 AM, Wolfgang Jeltsch
<[hidden email]> 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@.

--
Live well,
~wren
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users



_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Loading...