[GHC] #16263: Rework GHC's treatment of constraints in kinds

[GHC]

#16263: Rework GHC's treatment of constraints in kinds
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  simonpj
            Type:  bug               |               Status:  patch
        Priority:  normal            |            Milestone:  8.10.1
       Component:  Compiler          |              Version:  8.6.3
      Resolution:                    |             Keywords:  TypeInType,
                                     |  newcomer
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #12102, #15872    |  Differential Rev(s):
       Wiki Page:                    |  https://gitlab.haskell.org/ghc/ghc/merge_requests/128
-------------------------------------+-------------------------------------

Comment (by Marge Bot <ben+marge-bot@…>):

 In [changeset:"6cce36f83aec33d33545e0ef2135894d22dff5ca/ghc"
 6cce36f8/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="6cce36f83aec33d33545e0ef2135894d22dff5ca"
 Add AnonArgFlag to FunTy

 The big payload of this patch is:

   Add an AnonArgFlag to the FunTy constructor
   of Type, so that
     (FunTy VisArg   t1 t2) means (t1 -> t2)
     (FunTy InvisArg t1 t2) means (t1 => t2)

 The big payoff is that we have a simple, local test to make
 when decomposing a type, leading to many fewer calls to
 isPredTy. To me the code seems a lot tidier, and probably
 more efficient (isPredTy has to take the kind of the type).

 See Note [Function types] in TyCoRep.

 There are lots of consequences

 * I made FunTy into a record, so that it'll be easier
   when we add a linearity field, something that is coming
   down the road.

 * Lots of code gets touched in a routine way, simply because it
   pattern matches on FunTy.

 * I wanted to make a pattern synonym for (FunTy2 arg res), which
   picks out just the argument and result type from the record. But
   alas the pattern-match overlap checker has a heart attack, and
   either reports false positives, or takes too long.  In the end
   I gave up on pattern synonyms.

   There's some commented-out code in TyCoRep that shows what I
   wanted to do.

 * Much more clarity about predicate types, constraint types
   and (in particular) equality constraints in kinds.  See TyCoRep
   Note [Types for coercions, predicates, and evidence]
   and Note [Constraints in kinds].

   This made me realise that we need an AnonArgFlag on
   AnonTCB in a TyConBinder, something that was really plain
   wrong before. See TyCon Note [AnonTCB InivsArg]

 * When building function types we must know whether we
   need VisArg (mkVisFunTy) or InvisArg (mkInvisFunTy).
   This turned out to be pretty easy in practice.

 * Pretty-printing of types, esp in IfaceType, gets
   tidier, because we were already recording the (->)
   vs (=>) distinction in an ad-hoc way.  Death to
   IfaceFunTy.

 * mkLamType needs to keep track of whether it is building
   (t1 -> t2) or (t1 => t2).  See Type
   Note [mkLamType: dictionary arguments]

 Other minor stuff

 * Some tidy-up in validity checking involving constraints;
   Trac #16263
 }}}

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