[GHC] #13408: Consider inferring a higher-rank kind for type synonyms

Tue Oct 30 14:31:52 UTC 2018

#13408: Consider inferring a higher-rank kind for type synonyms
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 To be clear, I have no idea what "a little twiddling" constitutes in the
 slightest. The only clues I have are:

 * The
 [http://git.haskell.org/ghc.git/blob/0bdbbd4a637b169aa7043e0d9898ad1ecd5d14ef:/compiler/typecheck/TcBinds.hs#l1253
 code] around `Note [Single function non-recursive binding special-case]`
 looks relevant:

 {{{#!hs
                              -- Single function binding,
   | NonRecursive <- is_rec   -- ...binder isn't mentioned in RHS
   , Nothing <- sig_fn name   -- ...with no type signature
   =     -- Note [Single function non-recursive binding special-case]
         -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
         -- In this very special case we infer the type of the
         -- right hand side first (it may have a higher-rank type)
         -- and *then* make the monomorphic Id for the LHS
         -- e.g.         f = \(x::forall a. a->a) -> <body>
         --      We want to infer a higher-rank type for f
     setSrcSpan b_loc    $
     do  { ((co_fn, matches'), rhs_ty)
             <- tcInferInst $ \ exp_ty ->
                   -- tcInferInst: see TcUnify,
                   -- Note [Deep instantiation of InferResult]
                tcExtendBinderStack [TcIdBndr_ExpType name exp_ty
 NotTopLevel] $
                   -- We extend the error context even for a non-recursive
                   -- function so that in type error messages we show the
                   -- type of the thing whose rhs we are type checking
                tcMatchesFun (L nm_loc name) matches exp_ty

         ; ... }
 }}}

   I'm guessing that the type that you get from `tcInferInst` is important
 here.

 *
 [http://git.haskell.org/ghc.git/blob/849d3848f6a43c36eb0fffe45894be947ad66bfc:/compiler/typecheck/TcTyClsDecls.hs#l826
 This] appears to be the relevant code for kind-checking type synonyms:

 {{{#!hs
 getInitialKind decl@(SynDecl { tcdLName = L _ name
                              , tcdTyVars = ktvs
                              , tcdRhs = rhs })
   = do  { tycon <- kcLHsQTyVars name TypeSynonymFlavour (hsDeclHasCusk
 decl)
                                 ktvs $
             case kind_annotation rhs of
               Nothing -> newMetaKindVar
               Just ksig -> tcLHsKindSig (TySynKindCtxt name) ksig
         ; return [tycon] }
   where
     -- Keep this synchronized with 'hsDeclHasCusk'.
     kind_annotation (L _ ty) = case ty of
         HsParTy _ lty     -> kind_annotation lty
         HsKindSig _ _ k   -> Just k
         _                 -> Nothing
 }}}

   If I pass in the `[LTyClDecl GhcRn]` argument from `kcTyClGroup`, I can
 figure out if that type synonym is part of a recursive group or not.
 Similarly, if `kind_annotation rhs` returns `Nothing`, then I know that we
 don't have a CUSK. If those two things simultaneously hold true, then I'm
 in a situation where we should infer the overall kind.

   ...except that I'm not sure at all how to go about doing so. Several
 mysteries have presented itself:

   * Where exactly should `tcInferInst` go into this? Does the type that it
 give you in its callback refer to the overall kind of the type synonym?
 Just the return kind? Something else?
   * Once I have access to the type in `tcInferInst`, what do I even do
 with it? Do I pass it to `tcLHsKindSig`? Is there another function that's
 better suited to this situation?
   * `tcInferInst` also //returns// a type. What should I do with that?
   * Is the `tcExtendBinderStack` stuff from the term-level code relevant
 to this situation?

 Without some kind of direction, I'm very under-qualified to fix this, I'm
 afraid.

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