Opened 13 months ago

Closed 12 months ago

Last modified 11 months ago

#15591 closed bug (fixed)

Inconsistent kind variable binder visibility between associated and non-associated type families

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler Version: 8.5
Keywords: TypeApplications, TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: ghci/scripts/T15591
Blocked By: Blocking:
Related Tickets: #15592 Differential Rev(s): Phab:D5159
Wiki Page:

Description

Consider the following program and GHCi session which uses it:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where

import Data.Kind

type family T1 (x :: f (a :: Type))

class C (a :: Type) where
  type T2 (x :: f a)
$ ghc2/inplace/bin/ghc-stage2 --interactive Foo.hs -fprint-explicit-foralls
GHCi, version 8.7.20180831: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo              ( Foo.hs, interpreted )
Ok, one module loaded.
λ> :kind T1
T1 :: forall (f :: * -> *) a. f a -> *
λ> :kind T2
T2 :: forall {a} (f :: * -> *). f a -> *

Something is strange about the visibility of a in the kinds of T1 and T2. In T1, it's visible, but in T2, it's not! I would expect them to both be visible, since they were both mentioned by name in each type family's definition.

This isn't of much importance at the moment, but it will be once visible kind application lands, as this bug will prevent anyone from instantiating the a in T2 using a kind application.

I indicated 8.5 as the version for this ticket since this behavior has changed since GHC 8.4, where you'd get the following:

$ /opt/ghc/8.4.3/bin/ghci Foo.hs -fprint-explicit-foralls
GHCi, version 8.4.3: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo              ( Foo.hs, interpreted )
Ok, one module loaded.
λ> :kind T1
T1 :: forall (f :: * -> *) a. f a -> *
λ> :kind T2
T2 :: forall (f :: * -> *) a. f a -> *

Here, both as are visible. However, it's still wrong in that a should be listed before f in T2's telescope, since a was bound first (in C's class head), before f. In that sense, the current behavior is a slight improvement, although we're not fully correct yet.

The only difference between T1 and T2 is that T2 is associated with a class, which suggests that there is some difference in code paths between the two that is accounting for this.

Change History (14)

comment:1 Changed 13 months ago by RyanGlScott

I have somewhat of an idea why this is happening. The bindHsQTyVars function appears to be partly to blame for this discrepancy. bindHsQTyVars (which works over type families, among other things) computes kind variables like so:

implicit_kvs = filter_occs rdr_env bndrs kv_occs

Where filter_occs is defined as:

filter_occs :: LocalRdrEnv         -- In scope
            -> [Located RdrName]   -- Bound here
            -> [Located RdrName]   -- Potential implicit binders
            -> [Located RdrName]   -- Final implicit binders
-- Filter out any potential implicit binders that are either
-- already in scope, or are explicitly bound here
filter_occs rdr_env bndrs occs
  = filterOut is_in_scope occs
  where
    is_in_scope locc@(L _ occ) = isJust (lookupLocalRdrEnv rdr_env occ)
                              || locc `elemRdr` bndrs

Note that this filters out any type variable names which appear in rdr_env. This environment contains all type variables that have already been bound, which includes any variables that were bound by the class head. Therefore, in our original example, the a in class C (a :: Type) ends up being filtered out entirely, so by the time we get to typechecking, GHC thinks that a is an invisible argument.

One idea I had to fix this was to have filter_occs also return the class-bound variables so that they could be put at the front of the other kind variables. In other words, this patch:

  • compiler/rename/RnTypes.hs

    diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs
    index a78caaf..2163495 100644
    a b bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside 
    841841                                 -- Make sure to list the binder kvs before the
    842842                                 -- body kvs, as mandated by
    843843                                 -- Note [Ordering of implicit variables]
    844              implicit_kvs = filter_occs rdr_env bndrs kv_occs
     844             (cls_bound_nms, implicit_kvs) = filter_occs rdr_env bndrs kv_occs
    845845                                 -- Deleting bndrs: See Note [Kind-variable ordering]
    846846             -- dep_bndrs is the subset of bndrs that are dependent
    847847             --   i.e. appear in bndr/body_kv_occs
    bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside 
    858858                ]
    859859
    860860       ; implicit_kv_nms <- mapM (newTyVarNameRn mb_assoc) implicit_kvs
     861       ; let all_implicit_nms = cls_bound_nms ++ implicit_kv_nms
    861862
    862863       ; bindLocalNamesFV implicit_kv_nms                     $
    863864         bindLHsTyVarBndrs doc mb_in_doc mb_assoc hs_tv_bndrs $ \ rn_bndrs ->
    864865    do { traceRn "bindHsQTyVars" (ppr hsq_bndrs $$ ppr implicit_kv_nms $$ ppr rn_bndrs)
    865866       ; dep_bndr_nms <- mapM (lookupLocalOccRn . unLoc) dep_bndrs
    866867       ; thing_inside (HsQTvs { hsq_ext = HsQTvsRn
    867                                    { hsq_implicit  = implicit_kv_nms
     868                                   { hsq_implicit  = all_implicit_nms
    868869                                   , hsq_dependent = mkNameSet dep_bndr_nms }
    869870                              , hsq_explicit  = rn_bndrs })
    870871                      all_bound_on_lhs } }
    bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside 
    873874    filter_occs :: LocalRdrEnv         -- In scope
    874875                -> [Located RdrName]   -- Bound here
    875876                -> [Located RdrName]   -- Potential implicit binders
    876                 -> [Located RdrName]   -- Final implicit binders
     877                -> ([Name], [Located RdrName])
     878                     -- (Class binders, final implicit binders)
    877879    -- Filter out any potential implicit binders that are either
    878880    -- already in scope, or are explicitly bound here
    879881    filter_occs rdr_env bndrs occs
    880       = filterOut is_in_scope occs
     882      = partitionWith is_class_bound $
     883        filterOut is_implicit occs
    881884      where
    882         is_in_scope locc@(L _ occ) = isJust (lookupLocalRdrEnv rdr_env occ)
    883                                   || locc `elemRdr` bndrs
     885        is_class_bound :: Located RdrName
     886                       -> Either Name (Located RdrName)
     887                          -- Left: a class-bound name
     888                          -- Right: bound by the type family itself
     889        is_class_bound locc@(L _ occ) =
     890          case lookupLocalRdrEnv rdr_env occ of
     891            Just n  -> Left n
     892            Nothing -> Right locc
     893
     894        is_implicit :: Located RdrName -> Bool
     895        is_implicit locc = locc `elemRdr` bndrs
    884896
    885897{- Note [bindHsQTyVars examples]
    886898~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

That fixes the original program, encouragingly enough:

$ inplace/bin/ghc-stage2 --interactive ../Foo.hs -fprint-explicit-foralls
GHCi, version 8.7.20180831: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo              ( ../Foo.hs, interpreted )
Ok, one module loaded.
λ> :kind T2
T2 :: forall a (f :: * -> *). f a -> *

However, there's a catch. This causes a single test from the test suite to fail: T14131.

=====> T14131(normal) 1 of 1 [0, 0, 0]
cd "indexed-types/should_compile/T14131.run" &&  "/home/rgscott/Software/ghc2/inplace/test   spaces/ghc-stage2" -c T14131.hs -dcore-lint -dcmm-lint -no-user-package-db -rtsopts -fno-warn-missed-specialisations -fshow-warning-groups -fdiagnostics-color=never -fno-diagnostics-show-caret -dno-debug-output  
Compile failed (exit code 1) errors were:

T14131.hs:29:3: error:
    • Type indexes must match class instance head
      Expected: ZT
        Actual: ZT
      Use -fprint-explicit-kinds to see the kind arguments
    • In the class declaration for ‘Z’

*** unexpected failure for T14131(normal)

For reference, here's the full definition of ZT:

class Z k where
  type ZT :: Maybe k
  type ZT = (Nothing :: Maybe k)

If you do use -fprint-explicit-kinds, the results aren't much more informative:

[1 of 1] Compiling T14131           ( tests/indexed-types/should_compile/T14131.hs, interpreted )

tests/indexed-types/should_compile/T14131.hs:29:3: error:
    • Type indexes must match class instance head
      Expected: ZT k
        Actual: ZT k
    • In the class declaration for ‘Z’
   |
29 |   type ZT = (Nothing :: Maybe k)
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I'm still not sure what's going on here—more investigation is required.

comment:2 Changed 13 months ago by RyanGlScott

If nothing else, ZT has shown me that my patch in comment:1 isn't sufficient to fix the underlying issue in the first place. If I comment out the default equation for ZT, then :kind ZT still gives me forall {k}. Maybe k, with or without the patch. Back to the drawing board...

comment:3 Changed 13 months ago by RyanGlScott

Oops, it just hit me why I was getting forall {k}. Maybe k for ZT's kind even after the patch in comment:1ZT doesn't have a CUSK! (See #15592 for more on this point in particular.)

If I change the definition to this:

class Z (k :: Type) where
  type ZT :: Maybe k
  type ZT = (Nothing :: Maybe k)

Then I get forall k. Maybe k for the kind of ZT, as expected, and the default definition is no longer rejected. Yay!

But all is not well yet. There remains the mystery of why the CUSK-less version of ZT is being rejected after applying the patch in comment:1. One clue is that if I apply the patch in comment:1 (and comment out the default definition for ZT), then GHCi gives me the following kind for Z:

Z :: forall {k}. k -> Constraint

This doesn't seem right, since without the patch, I get the following kind for Z:

Z :: * -> Constraint

comment:4 Changed 13 months ago by simonpj

Let's agree the specification first. In this declaration

class C (a :: Type) where
  type T2 (x :: f a)

Then a is Required for C, but presumably it is only Specified for T2?

And what are the rules for Required/Specified/Inferred for type/class declarations that do not have a CUSK?

comment:5 Changed 13 months ago by goldfire

For comment:4's C, I would expect

C :: Type -> Constraint   -- a is required, but it's not mentioned by name in the kind
T2 :: forall (a :: Type) (f :: Type -> Type). f a -> Type

In T2's kind, I've put a first, because it was already in scope. This parallels the fact that class variables are quantified before other variables in polymorphic methods. Both a and f should be Specified, as they are user-written. The various Types in the kind of T2 arise from the defaulting behavior of open type families (unchanged in this conversation).

The specification of Specified/Inferred is very simple: if the user has written the variable name in the declaration, the variable is Specified. If not, it's Inferred.

As for the patch: I would expect that the solution to this problem would be in the type-checker, not the renamer. As it stands, I'm pretty sure that the renamer identifies the a in these associated type definitions with the same unique as the a in the class.

comment:6 Changed 13 months ago by simonpj

The specification of Specified/Inferred is very simple: if the user has written the variable name in the declaration, the variable is Specified. If not, it's Inferred.

Regardless of CUSK or non-CUSK? I think so, but let's say so explicitly.

comment:7 Changed 13 months ago by goldfire

Regardless of CUSK or non-CUSK.

comment:8 Changed 13 months ago by simonpj

Regardless of CUSK or non-CUSK.

Good. So one action is to add that to the user manual.

comment:9 in reply to:  5 Changed 13 months ago by RyanGlScott

Replying to goldfire:

As for the patch: I would expect that the solution to this problem would be in the type-checker, not the renamer. As it stands, I'm pretty sure that the renamer identifies the a in these associated type definitions with the same unique as the a in the class.

Well, it does identify the a in T2 to be the same a as in C. But after it does so, it immediately filters it out! That's problematic, because by the time you reach kcLHsQTyVars, the hsq_implicit field of the LHsQTyVars argument only contains fa is no longer within reach. (You can verify this for yourself by compiling this program with -ddump-tc-trace and searching for kcLHsQTyVars: cusk.)

comment:10 Changed 13 months ago by RyanGlScott

Milestone: 8.6.18.8.1

comment:11 Changed 12 months ago by RyanGlScott

Differential Rev(s): Phab:D5159
Status: newpatch

By gum, I think I figured out this one. The trick was to pass the type variables bound by the class directly kcLHsQTyVars and to use that to one's advantage. See Phab:D5159.

I still haven't figured out how to make the non-CUSK case for kcLHsQTyVars work yet (that code confuses the bejeezus out of me), but that's the topic of a separate ticket (#15592) anyway, so I'll leave that for later.

comment:12 Changed 12 months ago by Ryan Scott <ryan.gl.scott@…>

In a57fa247/ghc:

Quantify class variables first in associated families' kinds

Summary:
Previously, `kcLHsQTyVars` would always quantify class-bound
variables invisibly in the kinds of associated types, resulting in
#15591. We counteract this by explicitly passing the class-bound
variables to `kcLHsQTyVars` and quantifying over the ones that are
mentioned in the associated type such that (1) they are specified,
and (2) they come before other kind variables.
See `Note [Kind variable ordering for associated types]`.

Test Plan: make test TEST=T15591

Reviewers: goldfire, simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #15591

Differential Revision: https://phabricator.haskell.org/D5159

comment:13 Changed 12 months ago by RyanGlScott

Resolution: fixed
Status: patchclosed
Test Case: ghci/scripts/T15591

comment:14 Changed 11 months ago by Richard Eisenberg <rae@…>

In 5e45ad10/ghc:

Finish fix for #14880.

The real change that fixes the ticket is described in
Note [Naughty quantification candidates] in TcMType.

Fixing this required reworking candidateQTyVarsOfType, the function
that extracts free variables as candidates for quantification.
One consequence is that we now must be more careful when quantifying:
any skolems around must be quantified manually, and quantifyTyVars
will now only quantify over metavariables. This makes good sense,
as skolems are generally user-written and are listed in the AST.

As a bonus, we now have more control over the ordering of such
skolems.

Along the way, this commit fixes #15711 and refines the fix
to #14552 (by accepted a program that was previously rejected,
as we can now accept that program by zapping variables to Any).

This commit also does a fair amount of rejiggering kind inference
of datatypes. Notably, we now can skip the generalization step
in kcTyClGroup for types with CUSKs, because we get the
kind right the first time. This commit also thus fixes #15743 and
 #15592, which both concern datatype kind generalisation.
(#15591 is also very relevant.) For this aspect of the commit, see
Note [Required, Specified, and Inferred in types] in TcTyClsDecls.

Test cases: dependent/should_fail/T14880{,-2},
            dependent/should_fail/T15743[cd]
            dependent/should_compile/T15743{,e}
            ghci/scripts/T15743b
            polykinds/T15592
            dependent/should_fail/T15591[bc]
            ghci/scripts/T15591
Note: See TracTickets for help on using tickets.