Type families without CUSKs cannot be given visible kind variable binders

mentioned in issue #14880 (closed)

mentioned in issue #15591 (closed)

changed milestone to %8.6.1

changed weight to 5

added CUSKs Tbug Trac import labels

Yes, I would expect

In T1

* a is Specified
In T2

* k is Inferred

* a is Specified

See Note [TyVarBndrs, TyVarBinders, TyConBinders, and visibility] in TyCoRep.

Richard, what do you say?

(This will start to bite when we get visible kind application.)

I agree with ticket:15592#comment:159535. If a user writes the name of the variable, it is Specified. Thus, a is specified (in both declarations). k, unmentioned, is Inferred.

But I see some trouble ahead.

Consider

data VisProxy k (a :: k) = MkVP
class D (a :: Proxy j) (b :: Proxy k) c where
  meth1 :: forall z. D @j @k a b z => z -> Proxy '(a, b)
  meth2 :: Proxy k j -> Proxy '(a, b, c)

The constraint in meth1 looks like it's redundantly specifying that D should be instantiated at j and k. I say "redundantly" because D, without a CUSK, cannot be polymorphically recursive. However, we discover in meth2 that j actually depends on k. So (assuming inference succeeds at all, which I don't wish to debate here), we will get D :: forall (k :: Type) (j :: k). Proxy j -> Proxy k -> Type -> Constraint. (The Type in the third required argument to D comes from z's kind in meth1.)

Bottom line: any use of visible kind application should be considered to be an instance of polymorphic recursion, and thus should be banned in a mutually recursive group on a CUSK-less type. This is true even if the visible kind application is redundant.

Do you agree?

Bottom line: any use of visible kind application should be considered to be an instance of polymorphic recursion.

Yes, and we (presumably) have exactly same at the term level

reverse (xs :: [a]) = ...(reverse @a ys)....

This is illegal. When type checking reverse's RHS we have reverse :: alpha in the envt, and you can't type-apply that to anything. If we had a signature

reverse :: [b] -> [b]
reverse (xs :: [a]) = ...(reverse @a ys)....

that's fine, because the signature puts reverse :: forall b. [b] -> [b] into the envt.

This might be a useful example to add to the user-manual documetation for visible type application.

changed milestone to %8.8.1

Trac metadata

Trac field	Value
Related	- → #15591 (closed)

Ah, I now understand why non-CUSKed declarations seem to have totally different behavior with respect to visibility than CUSKed ones: their visibilities are determined in a completely different part of the code! In particular, in kcTyClGroup (as opposed to kcLHsQTyVars, which was the case for #15591 (closed)). These lines is quite relevant:

 ; kvs <- kindGeneralize (mkTyConKind tc_binders tc_res_kind)

 ; let all_binders = mkNamedTyConBinders Inferred kvs ++ tc_binders

It appears that all kind variables are simply made invisible, which is clearly not what we want. Now we just need to figure out how to bend this code to our will...

Hold off on this, please. I've tinkered some in this area en route to #14880 (closed) and don't want to duplicate effort.

Trac metadata

Trac field	Value
BlockedBy	- → #14880 (closed)

Ha ha. I looked at this too. Consider

data T f (a::k1) b = MkT (f a b)

Then we should get

T :: forall {k2} k1. (k1 -> k2 -> *) -> k1 -> k2 -> *

That is: k2 is Inferred but k1 is Specified. But neither is among the tc_binders of the TcTyCon that we make before kind-generalisation! Those tc_binders are only the Required ones, positionally written by the user. (It took me a while to work this out; we should write it down.)

OK so kindGeneralize will now generalise over both k1 and k1, in some random order. We must

Mark the Inferred ones as Inferred and similarly Specified.
Put the former before the latter

How can we distinguish? Well, the Specified ones are among the tcScopedTyVars of the TcTyCon, but the Inferred ones are not. So I did this, in kcTyClGroup:

           ; kvs <- kindGeneralize (mkTyConKind tc_binders tc_res_kind)

           ; scoped_tvs' <- zonkTyVarTyVarPairs scoped_tvs
           ; let (specified_kvs, inferred_kvs) = partition is_specified kvs
                 user_specified_tkvs = mkVarSet (map snd scoped_tvs')
                 is_specified kv = kv `elemVarSet` user_specified_tkvs
                 all_binders = mkNamedTyConBinders Inferred  inferred_kvs  ++
                               mkNamedTyConBinders Specified specified_kvs ++
                               tc_binders

This works.

I will not commit: over to you Richard.

That looks quite sensible and is independent from what I've done. (I was thinking we might have to put these into the tc_binders, but that's hard to get right for a non-CUSK.) If what you have works, feel free to commit. It won't get in my way.

By a series of strange coincidences, I ended up with almost exactly the same code as in ticket:15592#comment:160968 while working on this this morning. (Don't worry, I won't work on this any further until the dust has settled on #14880 (closed).) There's one thing I haven't worked out, though: how to make this work for associated types (in light of #15591 (closed)). Consider:

class C a where
  type T (x :: f a)

Ideally, the kind of T would be:

T :: forall {k} (a :: k) (f :: k -> Type). f a -> Type

Alas, the code in ticket:15592#comment:160968 is not enough to accomplish this. It will instead give this as the kind for T:

T :: forall {k} {a :: k} (f :: k -> Type). f a -> Type

Note that a is now invisible. Ack.

In order to fix this, we'd need to be aware of the fact that a is mentioned explicitly in C within kcTyClGroup. Currently, kcTyClGroup doesn't have access to this information, however.

Another gotcha is that if you only use the code in ticket:15592#comment:160968, it'll cause some programs to no longer typecheck. In particular, this program:

class C a where
  type T (x :: (f :: k -> Type) a)

Bug.hs:8:3: error:
    • These kind and type variables: (x :: (f :: k -> Type) a)
      are out of dependency order. Perhaps try this ordering:
        k (a :: k) (f :: k -> *) (x :: f a)
      NB: Implicitly declared variables come before others.
    • In the associated type family declaration for ‘T’
  |
8 |   type T (x :: (f :: k -> Type) a)
  |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I'm unclear if this is desirable or not.

In order to fix this, we'd need to be aware of the fact that a is mentioned explicitly in C within kcTyClGroup. Currently, kcTyClGroup doesn't have access to this information, however.

Hmm. I wonder if we should simply add a to the tyConScopedTyVars of T? And that info is available in kcLHsTQTVars which builds the TcTyCon. Richard?

Maybe that'd fix the gotcha too?

Replying to [ticket:15592#comment:161001 simonpj]:

Hmm. I wonder if we should simply add a to the tyConScopedTyVars of T? And that info is available in kcLHsTQTVars which builds the TcTyCon.

I too am a bit confused as to why we don't add a (or any kind variables, for that matter) to tcTyConScopedTyVars in the non-CUSK case of kcLHsQTyVars. The only reasoning I could find for this design choice is this terse comment:

       ; let   -- NB: Don't add scoped_kvs to tyConTyVars, because they
               -- must remain lined up with the binders
             tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs
             tycon = mkTcTyCon name (ppr user_tyvars) tc_binders res_kind
                               (mkTyVarNamePairs (scoped_kvs ++ tc_tvs))
                               flav

(Here, they call tcTyConScopedTyVars "tyConTyVars".)

I discovered that this bug fix has a visible effect! Consider this in GHC.Records:

-- | Constraint representing the fact that the field @x@ belongs to
-- the record type @r@ and has field type @a@.  This will be solved
-- automatically, but manual instances may be provided as well.
class HasField (x :: k) r a | x r -> a where
  -- | Selector function to extract the field from the record.
  getField :: r -> a

What is the kind of HasField and type of getField? As of today, GHC says

HasField :: forall {k}. k -> * -> * -> Constraint
getField :: forall {k] (x::k) r a. HasField x r a => r -> a

But actually, because of the (x :: k) in the class decl, the k is Specified. So the correct kind and type are:

HasField :: forall k. k -> * -> * -> Constraint
getField :: forall k (x::k) r a. HasField x r a => r -> a

So in a visible type application of getField you'd have to write getField @Symbol @x.

But that is not what Adam intended. We don't want to be forced to write that kind, even in a visible type application. We want k to be Inferred.

I can achieve this for now by changing the decl to

class HasField x r a | x r -> a where
  getField :: r -> a

so removing the :: k from the decl. But that is rather subtle. I'm looking forward to explicit kind signatures... but NB: they need to be able to express the Inferred/Specified distinction.

mentioned in commit 2f09753f

OK so I've done the first bit.

We still need to address ticket:15592#comment:160971

mentioned in issue #15743 (closed)

mentioned in commit 5e45ad10

After the commit in #15592 (closed), the program from ticket:15592#comment:160971:

class C a where
  type T (x :: (f :: k -> Type) a)

Now typechecks again. There doesn't appear to be a test case for this, however. Worth checking in?

I thought I did add this, though perhaps to a T15991 test. I'm out of cycles now for a few days, but please add if you can't find it.

mentioned in commit 42faeb3b

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Test case	- → polykinds/T15592{,b}

reopened

Concerning ticket:15592#comment:162930 we need to be careful

We certainly have C :: forall {k}. k -> Constraint. So k is Inferred and a is Required.

Now look at T. I think we want

T :: forall k (a::k) (f :: k->Type). f a -> Type

That is: k must be Specified (because the user wrote it); but it must precede the a which comes from the class. On the other hand, if T didn't mention k it'd be Inferred.

What about this?

class D (a::k) where
  type S a

Here k is Specified for D, but is it Specified or Inferred for S? The notes in Note [Required, Specified, and Inferred for types] do not really answer this question.

This business of thinking about how the class header affects the Inferred/Specified/Required spec for the associated type is desperately tricky. I still wonder if we should instead look at the type declaration alone.

An improvement would be this:

Whether the tyvar is Inferred or Specified is determined by looking at the associated type (alone)
But the order in which the Specified variables appear is affected by the class header.

Trac metadata

Trac field	Value
Resolution	ResolvedFixed → Unresolved

Richard and I talked more about this. We worried about

class C a b where
  type T (x :: b a)

In what order do T's Specified variables show up?

We got as far as a detailed proposal for associated types:

Which vars are Specified and which Inferred is determined by type decl alone (Specified = explicitly mentioned in the type decl)

• For the Specified variables:

Start with lexical order from type decl
Do a stable partition, moving the ones from the class decl to the front
Use ScopedSort to put them in dependency order.

But it all seemed terribly complicated. We ended up thinking that it'd be better to ingnore the class header, and just do the normal thing:

Start with the lexical order from the type decl
Use ScopedSort

This simplifies the spec, and simplifies the code.

It is a bit unlike what happens for class methods (where the class variables all show up at the front, but we have no idea how to do make associated types really behave like class methods. Eg

class C a where
 type F a

Then perhaps F :: forall a -> C a => Type, which is not ery nice. And it gets worse

class C a b where
  type F a

then perhaps F :: forall {b}. forall a -> C a b => Type. Ugh. But if b depends on a we'd have to put it later in the telescope.

So we decided to keep it simple! (This is a small change from the commit in #15592 (closed)).

Just to chime in agreement with ticket:15592#comment:163104. I'm sympathetic to the desire to put class variables first, but it gets ugly quickly. Here's another example:

class C a where
  type F (x :: (f :: k -> Type) a)

Here, k is actually a class variable, even though that's highly non-obvious. So k should go in the first clump of variables. But it would be easy to assume that k, not mentioned in the class header, goes with the second clump of variables.

In the end, I agreed that there are just too many wrinkles in the "class variables come first" design, and went with "infer variable order / visibility locally" instead.

mentioned in commit 2257a86d

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Test case	polykinds/T15592{,b} → polykinds/T15592, T15592b

mentioned in commit 17bd1635

A test case for ticket:15592#comment:159542 was added in 17bd163566153babbf51adaff8397f948ae363ca:

Author: mynguyen <mnguyen1@brynmawr.edu>
Date:   Tue Dec 18 11:52:26 2018 -0500

    Visible kind application
    
    Summary:
    This patch implements visible kind application (GHC Proposal 15/#12045), as well as #15360 and #15362.
    It also refactors unnamed wildcard handling, and requires that type equations in type families in Template Haskell be
    written with full type on lhs. PartialTypeSignatures are on and warnings are off automatically with visible kind
    application, just like in term-level.
    
    There are a few remaining issues with this patch, as documented in
    ticket #16082.
    
    Includes a submodule update for Haddock.
    
    Test Plan: Tests T12045a/b/c/TH1/TH2, T15362, T15592a
    
    Reviewers: simonpj, goldfire, bgamari, alanz, RyanGlScott, Iceland_jack
    
    Subscribers: ningning, Iceland_jack, RyanGlScott, int-index, rwbarton, mpickering, carter
    
    GHC Trac Issues: `#12045`, `#15362`, `#15592`, `#15788`, `#15793`, `#15795`, `#15797`, `#15799`, `#15801`, `#15807`, `#15816`
    
    Differential Revision: https://phabricator.haskell.org/D5229

Trac metadata

Trac field	Value
Test case	polykinds/T15592, T15592b → polykinds/T15592{b}, typecheck/should_fail/T15592a
Differential revisions	- → D5229

added TypeApplications TypeFamilies labels

added Pnormal label

Type families without CUSKs cannot be given visible kind variable binders

Child items 0

Activity

Type families without CUSKs cannot be given visible kind variable binders

Relates to

Activity