Opened 2 months ago

Closed 7 weeks ago

#15711 closed bug (fixed)

Kind inference of class variables does not examine associated types

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.6.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_compile/T15711
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

If I say this

{-# LANGUAGE TypeFamilies, PolyKinds, DataKinds #-}

module Bug where

class C a where
  type F (x :: Maybe a)

then GHCi says this

*Bug> :k C
C :: k -> Constraint

That's silly. C should have kind Type -> Constraint, because the usage of a in the kind of the associated type constraints a's kind.

Will fix.

Change History (3)

comment:1 Changed 7 weeks 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

comment:2 Changed 7 weeks ago by goldfire

It looks like I forgot to add a test case. If someone gets to this before I do, I'd be grateful. Perhaps tomorrow.

comment:3 Changed 7 weeks ago by goldfire

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_compile/T15711
Note: See TracTickets for help on using tickets.