[GHC] #15592: Type families without CUSKs cannot be given visible kind variable binders

GHC ghc-devs at haskell.org
Thu Nov 29 17:28:04 UTC 2018


#15592: Type families without CUSKs cannot be given visible kind variable binders
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.8.1
       Component:  Compiler          |              Version:  8.4.3
      Resolution:                    |             Keywords:
                                     |  TypeApplications, TypeFamilies,
                                     |  CUSKs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
                                     |  polykinds/T15592{,b}
      Blocked By:  14880             |             Blocking:
 Related Tickets:  #15591            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Simon Peyton Jones <simonpj@…>):

 In [changeset:"2257a86daa72db382eb927df12a718669d5491f8/ghc"
 2257a86d/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="2257a86daa72db382eb927df12a718669d5491f8"
 Taming the Kind Inference Monster

 My original goal was (Trac #15809) to move towards using level numbers
 as the basis for deciding which type variables to generalise, rather
 than searching for the free varaibles of the environment.  However
 it has turned into a truly major refactoring of the kind inference
 engine.

 Let's deal with the level-numbers part first:

 * Augment quantifyTyVars to calculate the type variables to
   quantify using level numbers, and compare the result with
   the existing approach.  That is; no change in behaviour,
   just a WARNing if the two approaches give different answers.

 * To do this I had to get the level number right when calling
   quantifyTyVars, and this entailed a bit of care, especially
   in the code for kind-checking type declarations.

 * However, on the way I was able to eliminate or simplify
   a number of calls to solveEqualities.

 This work is incomplete: I'm not /using/ level numbers yet.
 When I subsequently get rid of any remaining WARNings in
 quantifyTyVars, that the level-number answers differ from
 the current answers, then I can rip out the current
 "free vars of the environment" stuff.

 Anyway, this led me into deep dive into kind inference for type and
 class declarations, which is an increasingly soggy part of GHC.
 Richard already did some good work recently in

    commit 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3
    Date:   Thu Sep 13 09:56:02 2018 +0200

     Finish fix for #14880.

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

 but I kept turning over stones. So this patch has ended up
 with a pretty significant refactoring of that code too.

 Kind inference for types and classes
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 * Major refactoring in the way we generalise the inferred kind of
   a TyCon, in kcTyClGroup.  Indeed, I made it into a new top-level
   function, generaliseTcTyCon.  Plus a new Note to explain it
   Note [Inferring kinds for type declarations].

 * We decided (Trac #15592) not to treat class type variables specially
   when dealing with Inferred/Specified/Required for associated types.
   That simplifies things quite a bit. I also rewrote
   Note [Required, Specified, and Inferred for types]

 * Major refactoring of the crucial function kcLHsQTyVars:
   I split it into
        kcLHsQTyVars_Cusk  and  kcLHsQTyVars_NonCusk
   because the two are really quite different. The CUSK case is
   almost entirely rewritten, and is much easier because of our new
   decision not to treat the class variables specially

 * I moved all the error checks from tcTyClTyVars (which was a bizarre
   place for it) into generaliseTcTyCon and/or the CUSK case of
   kcLHsQTyVars.  Now tcTyClTyVars is extremely simple.

 * I got rid of all the all the subtleties in tcImplicitTKBndrs. Indeed
   now there is no difference between tcImplicitTKBndrs and
   kcImplicitTKBndrs; there is now a single bindImplicitTKBndrs.
   Same for kc/tcExplicitTKBndrs.  None of them monkey with level
   numbers, nor build implication constraints.  scopeTyVars is gone
   entirely, as is kcLHsQTyVarBndrs. It's vastly simpler.

   I found I could get rid of kcLHsQTyVarBndrs entirely, in favour of
   the bnew bindExplicitTKBndrs.

 Quantification
 ~~~~~~~~~~~~~~
 * I now deal with the "naughty quantification candidates"
   of the previous patch in candidateQTyVars, rather than in
   quantifyTyVars; see Note [Naughty quantification candidates]
   in TcMType.

   I also killed off closeOverKindsCQTvs in favour of the same
   strategy that we use for tyCoVarsOfType: namely, close over kinds
   at the occurrences.

   And candidateQTyVars no longer needs a gbl_tvs argument.

 * Passing the ContextKind, rather than the expected kind itself,
   to tc_hs_sig_type_and_gen makes it easy to allocate the expected
   result kind (when we are in inference mode) at the right level.

 Type families
 ~~~~~~~~~~~~~~
 * I did a major rewrite of the impenetrable tcFamTyPats. The result
   is vastly more comprehensible.

 * I got rid of kcDataDefn entirely, quite a big function.

 * I re-did the way that checkConsistentFamInst works, so
   that it allows alpha-renaming of invisible arguments.

 * The interaction of kind signatures and family instances is tricky.
     Type families: see Note [Apparently-nullary families]
     Data families: see Note [Result kind signature for a data family
 instance]
                    and Note [Eta-reduction for data families]

 * The consistent instantation of an associated type family is tricky.
   See Note [Checking consistent instantiation] and
       Note [Matching in the consistent-instantation check]
   in TcTyClsDecls.  It's now checked in TcTyClsDecls because that is
   when we have the relevant info to hand.

 * I got tired of the compromises in etaExpandFamInst, so I did the
   job properly by adding a field cab_eta_tvs to CoAxBranch.
   See Coercion.etaExpandCoAxBranch.

 tcInferApps and friends
 ~~~~~~~~~~~~~~~~~~~~~~~
 * I got rid of the mysterious and horrible ClsInstInfo argument
   to tcInferApps, checkExpectedKindX, and various checkValid
   functions.  It was horrible!

 * I got rid of [Type] result of tcInferApps.  This list was used
   only in tcFamTyPats, when checking the LHS of a type instance;
   and if there is a cast in the middle, the list is meaningless.
   So I made tcInferApps simpler, and moved the complexity
   (not much) to tcInferApps.

   Result: tcInferApps is now pretty comprehensible again.

 * I refactored the many function in TcMType that instantiate skolems.

 Smaller things

 * I rejigged the error message in checkValidTelescope; I think it's
   quite a bit better now.

 * checkValidType was not rejecting constraints in a kind signature
      forall (a :: Eq b => blah). blah2
   That led to further errors when we then do an ambiguity check.
   So I make checkValidType reject it more aggressively.

 * I killed off quantifyConDecl, instead calling kindGeneralize
   directly.

 * I fixed an outright bug in tyCoVarsOfImplic, where we were not
   colleting the tyvar of the kind of the skolems

 * Renamed ClsInstInfo to AssocInstInfo, and made it into its
   own data type

 * Some fiddling around with pretty-printing of family
   instances which was trickier than I thought.  I wanted
   wildcards to print as plain "_" in user messages, although
   they each need a unique identity in the CoAxBranch.

 Some other oddments

 * Refactoring around the trace messages from reportUnsolved.
 * A bit of extra tc-tracing in TcHsSyn.commitFlexi

 This patch fixes a raft of bugs, and includes tests for them.

  * #14887
  * #15740
  * #15764
  * #15789
  * #15804
  * #15817
  * #15870
  * #15874
  * #15881
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:23>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler


More information about the ghc-tickets mailing list