Miscellaneous improvements to `Convert` (#1020)

Now that Haddock is moving towards working entirely over `.hi` and `.hie` files,
all declarations and types are going to be synthesized via the `Convert` module.
In preparation for this change, here are a bunch of fixes to this module:

  * Add kind annotations to type variables in `forall`'s whose kind is not `Type`,
    unless the kind can be inferred from some later use of the variable. See
    `implicitForAll` and `noKindTyVars` in particular if you wish to dive into this.

  * Properly detect `HsQualTy` in `synifyType`. This is done by following suit with
    what GHC's `toIfaceTypeX` does and checking the first argument of
    `FunTy{} :: Type` to see if it classified as a given/wanted in the typechecker
    (see `isPredTy`). 

  * Beef up the logic around figuring out when an explicit `forall` is needed. This
    includes: observing if any of the type variables will need kind signatures, if the
    inferred type variable order _without_ a forall will still match the one GHC
    claims, and some other small things.

  * Add some (not yet used) functionality for default levity polymorphic type
    signatures. This functionality similar to `fprint-explicit-runtime-reps`.

Couple other smaller fixes only worth mentioning:

  * Show the family result signature only when it isn't `Type`
  * Fix rendering of implicit parameters in the LaTeX and Hoogle backends
  * Better handling of the return kind of polykinded H98 data declarations
  * Class decls produced by `tyThingToLHsDecl` now contain associated type
    defaults and default method signatures when appropriate
  * Filter out more `forall`'s in pattern synonyms

1 files changed, 322 insertions, 143 deletions

diff --git a/haddock-api/src/Haddock/Convert.hs b/haddock-api/src/Haddock/Convert.hs
index 5312bfc7..3d2e37b9 100644
--- a/haddock-api/src/Haddock/Convert.hs
+++ b/haddock-api/src/Haddock/Convert.hs
@@ -12,13 +12,16 @@
 -- Conversion between TyThing and HsDecl. This functionality may be moved into
 -- GHC at some point.
 -----------------------------------------------------------------------------
-module Haddock.Convert where
--- Some other functions turned out to be useful for converting
--- instance heads, which aren't TyThings, so just export everything.
+module Haddock.Convert (
+  tyThingToLHsDecl,
+  synifyInstHead,
+  synifyFamInst,
+  PrintRuntimeReps(..),
+) where
 
 import Bag ( emptyBag )
 import BasicTypes ( TupleSort(..), SourceText(..), LexicalFixity(..)
-                  , PromotionFlag(..) )
+                  , PromotionFlag(..), DefMethSpec(..) )
 import Class
 import CoAxiom
 import ConLike
@@ -49,12 +52,22 @@ import VarSet
 
 import Haddock.Types
 import Haddock.Interface.Specialize
+import Haddock.GhcUtils                      ( orderedFVs, defaultRuntimeRepVars )
 
+import Data.Maybe                            ( catMaybes, maybeToList )
 
 
+-- | Whether or not to default 'RuntimeRep' variables to 'LiftedRep'. Check
+-- out Note [Defaulting RuntimeRep variables] in IfaceType.hs for the
+-- motivation.
+data PrintRuntimeReps = ShowRuntimeRep | HideRuntimeRep deriving Show
+
 -- the main function here! yay!
-tyThingToLHsDecl :: TyThing -> Either ErrMsg ([ErrMsg], (HsDecl GhcRn))
-tyThingToLHsDecl t = case t of
+tyThingToLHsDecl
+  :: PrintRuntimeReps
+  -> TyThing
+  -> Either ErrMsg ([ErrMsg], (HsDecl GhcRn))
+tyThingToLHsDecl prr t = case t of
   -- ids (functions and zero-argument a.k.a. CAFs) get a type signature.
   -- Including built-in functions like seq.
   -- foreign-imported functions could be represented with ForD
@@ -63,40 +76,60 @@ tyThingToLHsDecl t = case t of
   -- in a future code version we could turn idVarDetails = foreign-call
   -- into a ForD instead of a SigD if we wanted.  Haddock doesn't
   -- need to care.
-  AnId i -> allOK $ SigD noExt (synifyIdSig ImplicitizeForAll i)
+  AnId i -> allOK $ SigD noExt (synifyIdSig prr ImplicitizeForAll [] i)
 
   -- type-constructors (e.g. Maybe) are complicated, put the definition
   -- later in the file (also it's used for class associated-types too.)
   ATyCon tc
     | Just cl <- tyConClass_maybe tc -- classes are just a little tedious
-    -> let extractFamilyDecl :: TyClDecl a -> Either ErrMsg (LFamilyDecl a)
-           extractFamilyDecl (FamDecl _ d) = return $ noLoc d
+    -> let extractFamilyDecl :: TyClDecl a -> Either ErrMsg (FamilyDecl a)
+           extractFamilyDecl (FamDecl _ d) = return d
            extractFamilyDecl _           =
              Left "tyThingToLHsDecl: impossible associated tycon"
 
-           atTyClDecls = [synifyTyCon Nothing at_tc | ATI at_tc _ <- classATItems cl]
-           atFamDecls  = map extractFamilyDecl (rights atTyClDecls)
-           tyClErrors = lefts atTyClDecls
-           famDeclErrors = lefts atFamDecls
-       in withErrs (tyClErrors ++ famDeclErrors) . TyClD noExt $ ClassDecl
+           extractFamDefDecl :: FamilyDecl GhcRn -> Type -> TyFamDefltEqn GhcRn
+           extractFamDefDecl fd rhs = FamEqn
+             { feqn_ext = noExt
+             , feqn_tycon = fdLName fd
+             , feqn_bndrs  = Nothing
+                 -- TODO: this must change eventually
+             , feqn_pats = fdTyVars fd
+             , feqn_fixity = fdFixity fd
+             , feqn_rhs = synifyType WithinType [] rhs }
+
+           extractAtItem
+             :: ClassATItem
+             -> Either ErrMsg (LFamilyDecl GhcRn, Maybe (LTyFamDefltEqn GhcRn))
+           extractAtItem (ATI at_tc def) = do
+             tyDecl <- synifyTyCon prr Nothing at_tc
+             famDecl <- extractFamilyDecl tyDecl
+             let defEqnTy = fmap (noLoc . extractFamDefDecl famDecl . fst) def
+             pure (noLoc famDecl, defEqnTy)
+
+           atTyClDecls = map extractAtItem (classATItems cl)
+           (atFamDecls, atDefFamDecls) = unzip (rights atTyClDecls)
+           vs = tyConVisibleTyVars (classTyCon cl)
+
+       in withErrs (lefts atTyClDecls) . TyClD noExt $ ClassDecl
          { tcdCtxt = synifyCtx (classSCTheta cl)
          , tcdLName = synifyName cl
-         , tcdTyVars = synifyTyVars (tyConVisibleTyVars (classTyCon cl))
-         , tcdFixity = Prefix
+         , tcdTyVars = synifyTyVars vs
+         , tcdFixity = synifyFixity cl
          , tcdFDs = map (\ (l,r) -> noLoc
                         (map (noLoc . getName) l, map (noLoc . getName) r) ) $
                          snd $ classTvsFds cl
          , tcdSigs = noLoc (MinimalSig noExt NoSourceText . noLoc . fmap noLoc $ classMinimalDef cl) :
-                      map (noLoc . synifyTcIdSig DeleteTopLevelQuantification)
-                        (classMethods cl)
+                      [ noLoc tcdSig
+                      | clsOp <- classOpItems cl
+                      , tcdSig <- synifyTcIdSig vs clsOp ]
          , tcdMeths = emptyBag --ignore default method definitions, they don't affect signature
          -- class associated-types are a subset of TyCon:
-         , tcdATs = rights atFamDecls
-         , tcdATDefs = [] --ignore associated type defaults
+         , tcdATs = atFamDecls
+         , tcdATDefs = catMaybes atDefFamDecls
          , tcdDocs = [] --we don't have any docs at this point
          , tcdCExt = placeHolderNamesTc }
     | otherwise
-    -> synifyTyCon Nothing tc >>= allOK . TyClD noExt
+    -> synifyTyCon prr Nothing tc >>= allOK . TyClD noExt
 
   -- type-constructors (e.g. Maybe) are complicated, put the definition
   -- later in the file (also it's used for class associated-types too.)
@@ -104,7 +137,7 @@ tyThingToLHsDecl t = case t of
 
   -- a data-constructor alone just gets rendered as a function:
   AConLike (RealDataCon dc) -> allOK $ SigD noExt (TypeSig noExt [synifyName dc]
-    (synifySigWcType ImplicitizeForAll (dataConUserType dc)))
+    (synifySigWcType ImplicitizeForAll [] (dataConUserType dc)))
 
   AConLike (PatSynCon ps) ->
     allOK . SigD noExt $ PatSynSig noExt [synifyName ps] (synifyPatSynSigType ps)
@@ -116,17 +149,17 @@ synifyAxBranch :: TyCon -> CoAxBranch -> TyFamInstEqn GhcRn
 synifyAxBranch tc (CoAxBranch { cab_tvs = tkvs, cab_lhs = args, cab_rhs = rhs })
   = let name            = synifyName tc
         args_types_only = filterOutInvisibleTypes tc args
-        typats          = map (synifyType WithinType) args_types_only
+        typats          = map (synifyType WithinType []) args_types_only
         annot_typats    = zipWith3 annotHsType (mkIsPolyTvs fam_tvs)
                                    args_types_only typats
-        hs_rhs          = synifyType WithinType rhs
+        hs_rhs          = synifyType WithinType [] rhs
     in HsIB { hsib_ext = map tyVarName tkvs
             , hsib_body   = FamEqn { feqn_ext    = noExt
                                    , feqn_tycon  = name
                                    , feqn_bndrs  = Nothing
-                                       -- this must change eventually
+                                       -- TODO: this must change eventually
                                    , feqn_pats   = map HsValArg annot_typats
-                                   , feqn_fixity = Prefix
+                                   , feqn_fixity = synifyFixity name
                                    , feqn_rhs    = hs_rhs } }
   where
     fam_tvs = tyConVisibleTyVars tc
@@ -141,42 +174,51 @@ synifyAxiom ax@(CoAxiom { co_ax_tc = tc })
 
   | Just ax' <- isClosedSynFamilyTyConWithAxiom_maybe tc
   , getUnique ax' == getUnique ax   -- without the getUniques, type error
-  = synifyTyCon (Just ax) tc >>= return . TyClD noExt
+  = synifyTyCon ShowRuntimeRep (Just ax) tc >>= return . TyClD noExt
 
   | otherwise
   = Left "synifyAxiom: closed/open family confusion"
 
--- | Turn type constructors into type class declarations
-synifyTyCon :: Maybe (CoAxiom br) -> TyCon -> Either ErrMsg (TyClDecl GhcRn)
-synifyTyCon _coax tc
+-- | Turn type constructors into data declarations, type families, or type synonyms
+synifyTyCon
+  :: PrintRuntimeReps
+  -> Maybe (CoAxiom br)  -- ^ RHS of type synonym
+  -> TyCon               -- ^ type constructor to convert
+  -> Either ErrMsg (TyClDecl GhcRn)
+synifyTyCon prr _coax tc
   | isFunTyCon tc || isPrimTyCon tc
   = return $
     DataDecl { tcdLName = synifyName tc
-             , tcdTyVars =       -- tyConTyVars doesn't work on fun/prim, but we can make them up:
-                         let mk_hs_tv realKind fakeTyVar
-                                = noLoc $ KindedTyVar noExt (noLoc (getName fakeTyVar))
-                                                      (synifyKindSig realKind)
-                         in HsQTvs { hsq_ext =
+             , tcdTyVars = HsQTvs { hsq_ext =
                                        HsQTvsRn { hsq_implicit = []   -- No kind polymorphism
                                                 , hsq_dependent = emptyNameSet }
-                                   , hsq_explicit = zipWith mk_hs_tv (fst (splitFunTys (tyConKind tc)))
-                                                                alphaTyVars --a, b, c... which are unfortunately all kind *
+                                   , hsq_explicit = zipWith mk_hs_tv
+                                                            tyVarKinds
+                                                            alphaTyVars --a, b, c... which are unfortunately all kind *
                                    }
 
-           , tcdFixity = Prefix
+           , tcdFixity = synifyFixity tc
 
            , tcdDataDefn = HsDataDefn { dd_ext = noExt
                                       , dd_ND = DataType  -- arbitrary lie, they are neither
                                                     -- algebraic data nor newtype:
                                       , dd_ctxt = noLoc []
                                       , dd_cType = Nothing
-                                      , dd_kindSig = Just (synifyKindSig (tyConKind tc))
+                                      , dd_kindSig = synifyDataTyConReturnKind tc
                                                -- we have their kind accurately:
                                       , dd_cons = []  -- No constructors
                                       , dd_derivs = noLoc [] }
            , tcdDExt = DataDeclRn False placeHolderNamesTc }
+  where
+    -- tyConTyVars doesn't work on fun/prim, but we can make them up:
+    mk_hs_tv realKind fakeTyVar
+      | isLiftedTypeKind realKind = noLoc $ UserTyVar noExt (noLoc (getName fakeTyVar))
+      | otherwise = noLoc $ KindedTyVar noExt (noLoc (getName fakeTyVar)) (synifyKindSig realKind)
+
+    conKind = defaultType prr (tyConKind tc)
+    tyVarKinds = fst . splitFunTys . snd . splitPiTysInvisible $ conKind
 
-synifyTyCon _coax tc
+synifyTyCon _prr _coax tc
   | Just flav <- famTyConFlav_maybe tc
   = case flav of
       -- Type families
@@ -200,7 +242,7 @@ synifyTyCon _coax tc
                  , fdInfo = i
                  , fdLName = synifyName tc
                  , fdTyVars = synifyTyVars (tyConVisibleTyVars tc)
-                 , fdFixity = Prefix
+                 , fdFixity = synifyFixity tc
                  , fdResultSig =
                        synifyFamilyResultSig resultVar (tyConResKind tc)
                  , fdInjectivityAnn =
@@ -208,13 +250,13 @@ synifyTyCon _coax tc
                                        (tyConInjectivityInfo tc)
                  }
 
-synifyTyCon coax tc
+synifyTyCon _prr coax tc
   | Just ty <- synTyConRhs_maybe tc
   = return $ SynDecl { tcdSExt   = emptyNameSet
                      , tcdLName  = synifyName tc
                      , tcdTyVars = synifyTyVars (tyConVisibleTyVars tc)
-                     , tcdFixity = Prefix
-                     , tcdRhs = synifyType WithinType ty }
+                     , tcdFixity = synifyFixity tc
+                     , tcdRhs = synifyType WithinType [] ty }
   | otherwise =
   -- (closed) newtype and data
   let
@@ -242,7 +284,7 @@ synifyTyCon coax tc
   -- That seems like an acceptable compromise (they'll just be documented
   -- in prefix position), since, otherwise, the logic (at best) gets much more
   -- complicated. (would use dataConIsInfix.)
-  use_gadt_syntax = any (not . isVanillaDataCon) (tyConDataCons tc)
+  use_gadt_syntax = isGadtSyntaxTyCon tc
   consRaw = map (synifyDataCon use_gadt_syntax) (tyConDataCons tc)
   cons = rights consRaw
   -- "deriving" doesn't affect the signature, no need to specify any.
@@ -256,31 +298,31 @@ synifyTyCon coax tc
                     , dd_derivs  = alg_deriv }
  in case lefts consRaw of
   [] -> return $
-        DataDecl { tcdLName = name, tcdTyVars = tyvars, tcdFixity = Prefix
+        DataDecl { tcdLName = name, tcdTyVars = tyvars
+                 , tcdFixity = synifyFixity name
                  , tcdDataDefn = defn
                  , tcdDExt = DataDeclRn False placeHolderNamesTc }
   dataConErrs -> Left $ unlines dataConErrs
 
--- In this module, every TyCon being considered has come from an interface
+-- | In this module, every TyCon being considered has come from an interface
 -- file. This means that when considering a data type constructor such as:
 --
---   data Foo (w :: *) (m :: * -> *) (a :: *)
+-- > data Foo (w :: *) (m :: * -> *) (a :: *)
 --
 -- Then its tyConKind will be (* -> (* -> *) -> * -> *). But beware! We are
 -- also rendering the type variables of Foo, so if we synify the tyConKind of
 -- Foo in full, we will end up displaying this in Haddock:
 --
---   data Foo (w :: *) (m :: * -> *) (a :: *)
---     :: * -> (* -> *) -> * -> *
+-- > data Foo (w :: *) (m :: * -> *) (a :: *)
+-- >   :: * -> (* -> *) -> * -> *
 --
--- Which is entirely wrong (#548). We only want to display the *return* kind,
+-- Which is entirely wrong (#548). We only want to display the /return/ kind,
 -- which this function obtains.
 synifyDataTyConReturnKind :: TyCon -> Maybe (LHsKind GhcRn)
 synifyDataTyConReturnKind tc
-  = case splitFunTys (tyConKind tc) of
-      (_, ret_kind)
-        | isLiftedTypeKind ret_kind -> Nothing -- Don't bother displaying :: *
-        | otherwise                 -> Just (synifyKindSig ret_kind)
+  | isLiftedTypeKind ret_kind = Nothing -- Don't bother displaying :: *
+  | otherwise                 = Just (synifyKindSig ret_kind)
+  where ret_kind = tyConResKind tc
 
 synifyInjectivityAnn :: Maybe Name -> [TyVar] -> Injectivity
                      -> Maybe (LInjectivityAnn GhcRn)
@@ -291,8 +333,9 @@ synifyInjectivityAnn (Just lhs) tvs (Injective inj) =
     in Just $ noLoc $ InjectivityAnn (noLoc lhs) rhs
 
 synifyFamilyResultSig :: Maybe Name -> Kind -> LFamilyResultSig GhcRn
-synifyFamilyResultSig  Nothing    kind =
-   noLoc $ KindSig  noExt (synifyKindSig kind)
+synifyFamilyResultSig  Nothing    kind
+   | isLiftedTypeKind kind = noLoc $ NoSig noExt
+   | otherwise = noLoc $ KindSig  noExt (synifyKindSig kind)
 synifyFamilyResultSig (Just name) kind =
    noLoc $ TyVarSig noExt (noLoc $ KindedTyVar noExt (noLoc name) (synifyKindSig kind))
 
@@ -313,11 +356,12 @@ synifyDataCon use_gadt_syntax dc =
   (univ_tvs, ex_tvs, _eq_spec, theta, arg_tys, res_ty) = dataConFullSig dc
 
   -- skip any EqTheta, use 'orig'inal syntax
-  ctx = synifyCtx theta
+  ctx | null theta = Nothing
+      | otherwise = Just $ synifyCtx theta
 
   linear_tys =
     zipWith (\ty bang ->
-               let tySyn = synifyType WithinType ty
+               let tySyn = synifyType WithinType [] ty
                in case bang of
                     (HsSrcBang _ NoSrcUnpack NoSrcStrict) -> tySyn
                     bang' -> noLoc $ HsBangTy noExt bang' tySyn)
@@ -341,33 +385,55 @@ synifyDataCon use_gadt_syntax dc =
            then return $ noLoc $
               ConDeclGADT { con_g_ext  = noExt
                           , con_names  = [name]
-                          , con_forall = noLoc True
+                          , con_forall = noLoc False
                           , con_qvars  = synifyTyVars (univ_tvs ++ ex_tvs)
-                          , con_mb_cxt = Just ctx
-                          , con_args   =  hat
-                          , con_res_ty = synifyType WithinType res_ty
-                          , con_doc    =  Nothing }
+                          , con_mb_cxt = ctx
+                          , con_args   = hat
+                          , con_res_ty = synifyType WithinType [] res_ty
+                          , con_doc    = Nothing }
            else return $ noLoc $
               ConDeclH98 { con_ext    = noExt
                          , con_name   = name
-                         , con_forall = noLoc True
+                         , con_forall = noLoc False
                          , con_ex_tvs = map synifyTyVar ex_tvs
-                         , con_mb_cxt = Just ctx
+                         , con_mb_cxt = ctx
                          , con_args   = hat
                          , con_doc    = Nothing }
 
 synifyName :: NamedThing n => n -> Located Name
 synifyName n = L (srcLocSpan (getSrcLoc n)) (getName n)
 
-
-synifyIdSig :: SynifyTypeState -> Id -> Sig GhcRn
-synifyIdSig s i = TypeSig noExt [synifyName i] (synifySigWcType s (varType i))
-
-synifyTcIdSig :: SynifyTypeState -> Id -> Sig GhcRn
-synifyTcIdSig s i = ClassOpSig noExt False [synifyName i] (synifySigType s (varType i))
+-- | Guess the fixity of a something with a name. This isn't quite right, since
+-- a user can always declare an infix name in prefix form or a prefix name in
+-- infix form. Unfortunately, that is not something we can usually reconstruct.
+synifyFixity :: NamedThing n => n -> LexicalFixity
+synifyFixity n | isSymOcc (getOccName n) = Infix
+               | otherwise = Prefix
+
+synifyIdSig
+  :: PrintRuntimeReps -- ^ are we printing tyvars of kind 'RuntimeRep'?
+  -> SynifyTypeState  -- ^ what to do with a 'forall'
+  -> [TyVar]          -- ^ free variables in the type to convert
+  -> Id               -- ^ the 'Id' from which to get the type signature
+  -> Sig GhcRn
+synifyIdSig prr s vs i = TypeSig noExt [synifyName i] (synifySigWcType s vs t)
+  where
+    t = defaultType prr (varType i)
+
+-- | Turn a 'ClassOpItem' into a list of signatures. The list returned is going
+-- to contain the synified 'ClassOpSig' as well (when appropriate) a default
+-- 'ClassOpSig'.
+synifyTcIdSig :: [TyVar] -> ClassOpItem -> [Sig GhcRn]
+synifyTcIdSig vs (i, dm) =
+  [ ClassOpSig noExt False [synifyName i] (mainSig (varType i)) ] ++
+  [ ClassOpSig noExt True [noLoc dn] (defSig dt)
+  | Just (dn, GenericDM dt) <- [dm] ]
+  where
+    mainSig t = synifySigType DeleteTopLevelQuantification vs t
+    defSig t = synifySigType ImplicitizeForAll vs t
 
 synifyCtx :: [PredType] -> LHsContext GhcRn
-synifyCtx = noLoc . map (synifyType WithinType)
+synifyCtx = noLoc . map (synifyType WithinType [])
 
 
 synifyTyVars :: [TyVar] -> LHsQTyVars GhcRn
@@ -376,13 +442,20 @@ synifyTyVars ktvs = HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = []
                            , hsq_explicit = map synifyTyVar ktvs }
 
 synifyTyVar :: TyVar -> LHsTyVarBndr GhcRn
-synifyTyVar tv
-  | isLiftedTypeKind kind = noLoc (UserTyVar noExt (noLoc name))
-  | otherwise             = noLoc (KindedTyVar noExt (noLoc name) (synifyKindSig kind))
+synifyTyVar = synifyTyVar' emptyVarSet
+
+-- | Like 'synifyTyVar', but accepts a set of variables for which to omit kind
+-- signatures (even if they don't have the lifted type kind).
+synifyTyVar' :: VarSet -> TyVar -> LHsTyVarBndr GhcRn
+synifyTyVar' no_kinds tv
+  | isLiftedTypeKind kind || tv `elemVarSet` no_kinds
+  = noLoc (UserTyVar noExt (noLoc name))
+  | otherwise = noLoc (KindedTyVar noExt (noLoc name) (synifyKindSig kind))
   where
     kind = tyVarKind tv
     name = getName tv
 
+
 -- | Annotate (with HsKingSig) a type if the first parameter is True
 -- and if the type contains a free variable.
 -- This is used to synify type patterns for poly-kinded tyvars in
@@ -394,7 +467,7 @@ annotHsType _    _  hs_ty@(L _ (HsKindSig {})) = hs_ty
 annotHsType True ty hs_ty
   | not $ isEmptyVarSet $ filterVarSet isTyVar $ tyCoVarsOfType ty
   = let ki    = typeKind ty
-        hs_ki = synifyType WithinType ki
+        hs_ki = synifyType WithinType [] ki
     in noLoc (HsKindSig noExt hs_ty hs_ki)
 annotHsType _    _ hs_ty = hs_ty
 
@@ -417,7 +490,8 @@ data SynifyTypeState
   -- quite understand what's going on.
   | ImplicitizeForAll
   -- ^ beginning of a function definition, in which, to make it look
-  --   less ugly, those rank-1 foralls are made implicit.
+  --   less ugly, those rank-1 foralls (without kind annotations) are made
+  --   implicit.
   | DeleteTopLevelQuantification
   -- ^ because in class methods the context is added to the type
   --   (e.g. adding @forall a. Num a =>@ to @(+) :: a -> a -> a@)
@@ -426,22 +500,33 @@ data SynifyTypeState
   --   the defining class gets to quantify all its functions for free!
 
 
-synifySigType :: SynifyTypeState -> Type -> LHsSigType GhcRn
+synifySigType :: SynifyTypeState -> [TyVar] -> Type -> LHsSigType GhcRn
 -- The empty binders is a bit suspicious;
 -- what if the type has free variables?
-synifySigType s ty = mkEmptyImplicitBndrs (synifyType s ty)
+synifySigType s vs ty = mkEmptyImplicitBndrs (synifyType s vs ty)
 
-synifySigWcType :: SynifyTypeState -> Type -> LHsSigWcType GhcRn
+synifySigWcType :: SynifyTypeState -> [TyVar] -> Type -> LHsSigWcType GhcRn
 -- Ditto (see synifySigType)
-synifySigWcType s ty = mkEmptyWildCardBndrs (mkEmptyImplicitBndrs (synifyType s ty))
+synifySigWcType s vs ty = mkEmptyWildCardBndrs (mkEmptyImplicitBndrs (synifyType s vs ty))
 
 synifyPatSynSigType :: PatSyn -> LHsSigType GhcRn
 -- Ditto (see synifySigType)
 synifyPatSynSigType ps = mkEmptyImplicitBndrs (synifyPatSynType ps)
 
-synifyType :: SynifyTypeState -> Type -> LHsType GhcRn
-synifyType _ (TyVarTy tv) = noLoc $ HsTyVar noExt NotPromoted $ noLoc (getName tv)
-synifyType _ (TyConApp tc tys)
+-- | Depending on the first argument, try to default all type variables of kind
+-- 'RuntimeRep' to 'LiftedType'.
+defaultType :: PrintRuntimeReps -> Type -> Type
+defaultType ShowRuntimeRep = id
+defaultType HideRuntimeRep = defaultRuntimeRepVars
+
+-- | Convert a core type into an 'HsType'.
+synifyType
+  :: SynifyTypeState  -- ^ what to do with a 'forall'
+  -> [TyVar]          -- ^ free variables in the type to convert
+  -> Type             -- ^ the type to convert
+  -> LHsType GhcRn
+synifyType _ _ (TyVarTy tv) = noLoc $ HsTyVar noExt NotPromoted $ noLoc (getName tv)
+synifyType _ vs (TyConApp tc tys)
   = maybe_sig res_ty
   where
     res_ty :: LHsType GhcRn
@@ -459,21 +544,21 @@ synifyType _ (TyConApp tc tys)
                               BoxedTuple      -> HsBoxedTuple
                               ConstraintTuple -> HsConstraintTuple
                               UnboxedTuple    -> HsUnboxedTuple)
-                           (map (synifyType WithinType) vis_tys)
-      | isUnboxedSumTyCon tc = noLoc $ HsSumTy noExt (map (synifyType WithinType) vis_tys)
+                           (map (synifyType WithinType vs) vis_tys)
+      | isUnboxedSumTyCon tc = noLoc $ HsSumTy noExt (map (synifyType WithinType vs) vis_tys)
       | Just dc <- isPromotedDataCon_maybe tc
       , isTupleDataCon dc
       , dataConSourceArity dc == length vis_tys
-      = noLoc $ HsExplicitTupleTy noExt (map (synifyType WithinType) vis_tys)
+      = noLoc $ HsExplicitTupleTy noExt (map (synifyType WithinType vs) vis_tys)
       -- ditto for lists
       | getName tc == listTyConName, [ty] <- vis_tys =
-         noLoc $ HsListTy noExt (synifyType WithinType ty)
+         noLoc $ HsListTy noExt (synifyType WithinType vs ty)
       | tc == promotedNilDataCon, [] <- vis_tys
       = noLoc $ HsExplicitListTy noExt IsPromoted []
       | tc == promotedConsDataCon
       , [ty1, ty2] <- vis_tys
-      = let hTy = synifyType WithinType ty1
-        in case synifyType WithinType ty2 of
+      = let hTy = synifyType WithinType vs ty1
+        in case synifyType WithinType vs ty2 of
              tTy | L _ (HsExplicitListTy _ IsPromoted tTy') <- stripKindSig tTy
                  -> noLoc $ HsExplicitListTy noExt IsPromoted (hTy : tTy')
                  | otherwise
@@ -482,21 +567,21 @@ synifyType _ (TyConApp tc tys)
       | tc `hasKey` ipClassKey
       , [name, ty] <- tys
       , Just x <- isStrLitTy name
-      = noLoc $ HsIParamTy noExt (noLoc $ HsIPName x) (synifyType WithinType ty)
+      = noLoc $ HsIParamTy noExt (noLoc $ HsIPName x) (synifyType WithinType vs ty)
       -- and equalities
       | tc `hasKey` eqTyConKey
       , [ty1, ty2] <- tys
       = noLoc $ HsOpTy noExt
-                       (synifyType WithinType ty1)
+                       (synifyType WithinType vs ty1)
                        (noLoc eqTyConName)
-                       (synifyType WithinType ty2)
+                       (synifyType WithinType vs ty2)
       -- and infix type operators
       | isSymOcc (nameOccName (getName tc))
       , ty1:ty2:tys_rest <- vis_tys
       = mk_app_tys (HsOpTy noExt
-                           (synifyType WithinType ty1)
+                           (synifyType WithinType vs ty1)
                            (noLoc $ getName tc)
-                           (synifyType WithinType ty2))
+                           (synifyType WithinType vs ty2))
                    tys_rest
       -- Most TyCons:
       | otherwise
@@ -507,7 +592,7 @@ synifyType _ (TyConApp tc tys)
         mk_app_tys ty_app ty_args =
           foldl (\t1 t2 -> noLoc $ HsAppTy noExt t1 t2)
                 (noLoc ty_app)
-                (map (synifyType WithinType) $
+                (map (synifyType WithinType vs) $
                  filterOut isCoercionTy ty_args)
 
     vis_tys  = filterOutInvisibleTypes tc tys
@@ -518,7 +603,7 @@ synifyType _ (TyConApp tc tys)
     maybe_sig ty'
       | needs_kind_sig
       = let full_kind  = typeKind (mkTyConApp tc tys)
-            full_kind' = synifyType WithinType full_kind
+            full_kind' = synifyType WithinType vs full_kind
         in noLoc $ HsKindSig noExt ty' full_kind'
       | otherwise = ty'
 
@@ -536,80 +621,174 @@ synifyType _ (TyConApp tc tys)
 
         in not (subVarSet result_vars dropped_vars)
 
-synifyType s (AppTy t1 (CoercionTy {})) = synifyType s t1
-synifyType _ (AppTy t1 t2) = let
-  s1 = synifyType WithinType t1
-  s2 = synifyType WithinType t2
+synifyType s vs (AppTy t1 (CoercionTy {})) = synifyType s vs t1
+synifyType _ vs (AppTy t1 t2) = let
+  s1 = synifyType WithinType vs t1
+  s2 = synifyType WithinType vs t2
   in noLoc $ HsAppTy noExt s1 s2
-synifyType _ (FunTy t1 t2) = let
-  s1 = synifyType WithinType t1
-  s2 = synifyType WithinType t2
-  in noLoc $ HsFunTy noExt s1 s2
-synifyType s forallty@(ForAllTy _tv _ty) =
-  let (tvs, ctx, tau) = tcSplitSigmaTyPreserveSynonyms forallty
+synifyType s vs funty@(FunTy t1 t2)
+  | isPredTy t1 = synifyForAllType s vs funty
+  | otherwise = let s1 = synifyType WithinType vs t1
+                    s2 = synifyType WithinType vs t2
+                in noLoc $ HsFunTy noExt s1 s2
+synifyType s vs forallty@(ForAllTy _tv _ty) = synifyForAllType s vs forallty
+
+synifyType _ _ (LitTy t) = noLoc $ HsTyLit noExt $ synifyTyLit t
+synifyType s vs (CastTy t _) = synifyType s vs t
+synifyType _ _ (CoercionTy {}) = error "synifyType:Coercion"
+
+-- | Process a 'Type' which starts with a forall or a constraint into
+-- an 'HsType'
+synifyForAllType
+  :: SynifyTypeState  -- ^ what to do with the 'forall'
+  -> [TyVar]          -- ^ free variables in the type to convert
+  -> Type             -- ^ the forall type to convert
+  -> LHsType GhcRn
+synifyForAllType s vs ty =
+  let (tvs, ctx, tau) = tcSplitSigmaTyPreserveSynonyms ty
       sPhi = HsQualTy { hst_ctxt = synifyCtx ctx
-                      , hst_xqual   = noExt
-                      , hst_body = synifyType WithinType tau }
+                      , hst_xqual = noExt
+                      , hst_body = synifyType WithinType (tvs' ++ vs) tau }
+
+      sTy = HsForAllTy { hst_bndrs = sTvs
+                       , hst_xforall = noExt
+                       , hst_body  = noLoc sPhi }
+
+      sTvs = map synifyTyVar tvs
+
+      -- Figure out what the type variable order would be inferred in the
+      -- absence of an explicit forall
+      tvs' = orderedFVs (mkVarSet vs) (ctx ++ [tau])
+
   in case s of
-    DeleteTopLevelQuantification -> synifyType ImplicitizeForAll tau
-    WithinType        -> noLoc $ HsForAllTy { hst_bndrs = map synifyTyVar tvs
-                                            , hst_xforall = noExt
-                                            , hst_body  = noLoc sPhi }
-    ImplicitizeForAll -> noLoc sPhi
+    DeleteTopLevelQuantification -> synifyType ImplicitizeForAll (tvs' ++ vs) tau
+
+    -- Put a forall in if there are any type variables
+    WithinType
+      | not (null tvs) -> noLoc sTy
+      | otherwise -> noLoc sPhi
+
+    ImplicitizeForAll -> implicitForAll [] vs tvs ctx (synifyType WithinType) tau
+
+
+-- | Put a forall in if there are any type variables which require
+-- explicit kind annotations or if the inferred type variable order
+-- would be different.
+implicitForAll
+  :: [TyCon]          -- ^ type constructors that determine their args kinds
+  -> [TyVar]          -- ^ free variables in the type to convert
+  -> [TyVar]          -- ^ type variable binders in the forall
+  -> ThetaType        -- ^ constraints right after the forall
+  -> ([TyVar] -> Type -> LHsType GhcRn) -- ^ how to convert the inner type
+  -> Type             -- ^ inner type
+  -> LHsType GhcRn
+implicitForAll tycons vs tvs ctx synInner tau
+  | any (isHsKindedTyVar . unLoc) sTvs = noLoc sTy
+  | tvs' /= tvs                        = noLoc sTy
+  | otherwise                          = noLoc sPhi
+  where
+  sRho = synInner (tvs' ++ vs) tau
+  sPhi | null ctx = unLoc sRho
+       | otherwise
+       = HsQualTy { hst_ctxt = synifyCtx ctx
+                  , hst_xqual = noExt
+                  , hst_body = synInner (tvs' ++ vs) tau }
+  sTy = HsForAllTy { hst_bndrs = sTvs
+                   , hst_xforall = noExt
+                   , hst_body = noLoc sPhi }
+
+  no_kinds_needed = noKindTyVars tycons tau
+  sTvs = map (synifyTyVar' no_kinds_needed) tvs
+
+  -- Figure out what the type variable order would be inferred in the
+  -- absence of an explicit forall
+  tvs' = orderedFVs (mkVarSet vs) (ctx ++ [tau])
 
-synifyType _ (LitTy t) = noLoc $ HsTyLit noExt $ synifyTyLit t
-synifyType s (CastTy t _) = synifyType s t
-synifyType _ (CoercionTy {}) = error "synifyType:Coercion"
+
+
+-- | Find the set of type variables whose kind signatures can be properly
+-- inferred just from their uses in the type signature. This means the type
+-- variable to has at least one fully applied use @f x1 x2 ... xn@ where:
+--
+--   * @f@ has a function kind where the arguments have the same kinds
+--     as @x1 x2 ... xn@.
+--
+--   * @f@ has a function kind whose final return has lifted type kind
+--
+noKindTyVars
+  :: [TyCon]  -- ^ type constructors that determine their args kinds
+  -> Type     -- ^ type to inspect
+  -> VarSet   -- ^ set of variables whose kinds can be inferred from uses in the type
+noKindTyVars _ (TyVarTy var)
+  | isLiftedTypeKind (tyVarKind var) = unitVarSet var
+noKindTyVars ts ty
+  | (f, xs) <- splitAppTys ty
+  , not (null xs)
+  = let args = map (noKindTyVars ts) xs
+        func = case f of
+                 TyVarTy var | (xsKinds, outKind) <- splitFunTys (tyVarKind var)
+                             , xsKinds `eqTypes` map typeKind xs
+                             , isLiftedTypeKind outKind
+                             -> unitVarSet var
+                 TyConApp t ks | t `elem` ts
+                               , all noFreeVarsOfType ks
+                               -> mkVarSet [ v | TyVarTy v <- xs ]
+                 _ -> noKindTyVars ts f
+    in unionVarSets (func : args)
+noKindTyVars ts (ForAllTy _ t) = noKindTyVars ts t
+noKindTyVars ts (FunTy t1 t2) = noKindTyVars ts t1 `unionVarSet` noKindTyVars ts t2
+noKindTyVars ts (CastTy t _) = noKindTyVars ts t
+noKindTyVars _ _ = emptyVarSet
 
 synifyPatSynType :: PatSyn -> LHsType GhcRn
-synifyPatSynType ps = let
-  (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, res_ty) = patSynSig ps
-  req_theta' | null req_theta && not (null prov_theta && null ex_tvs) = [unitTy]
-               -- HACK: a HsQualTy with theta = [unitTy] will be printed as "() =>",
-               -- i.e., an explicit empty context, which is what we need. This is not
-               -- possible by taking theta = [], as that will print no context at all
-             | otherwise = req_theta
-  sForAll []  s = s
-  sForAll tvs s = HsForAllTy { hst_bndrs   = map synifyTyVar tvs
-                             , hst_xforall = noExt
-                             , hst_body    = noLoc s }
-  sQual theta s = HsQualTy   { hst_ctxt    = synifyCtx theta
-                             , hst_xqual   = noExt
-                             , hst_body    = noLoc s }
-  sTau = unLoc $ synifyType WithinType $ mkFunTys arg_tys res_ty
-  in noLoc $ sForAll univ_tvs $ sQual req_theta' $ sForAll ex_tvs $ sQual prov_theta sTau
+synifyPatSynType ps =
+  let (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, res_ty) = patSynSig ps
+      ts = maybeToList (tyConAppTyCon_maybe res_ty)
+
+      -- HACK: a HsQualTy with theta = [unitTy] will be printed as "() =>",
+      -- i.e., an explicit empty context, which is what we need. This is not
+      -- possible by taking theta = [], as that will print no context at all
+      req_theta' | null req_theta
+                 , not (null prov_theta && null ex_tvs)
+                 = [unitTy]
+                 | otherwise = req_theta
+
+  in implicitForAll ts [] (univ_tvs ++ ex_tvs) req_theta'
+       (\vs -> implicitForAll ts vs [] prov_theta (synifyType WithinType))
+       (mkFunTys arg_tys res_ty)
 
 synifyTyLit :: TyLit -> HsTyLit
 synifyTyLit (NumTyLit n) = HsNumTy NoSourceText n
 synifyTyLit (StrTyLit s) = HsStrTy NoSourceText s
 
 synifyKindSig :: Kind -> LHsKind GhcRn
-synifyKindSig k = synifyType WithinType k
+synifyKindSig k = synifyType WithinType [] k
 
 stripKindSig :: LHsType GhcRn -> LHsType GhcRn
 stripKindSig (L _ (HsKindSig _ t _)) = t
 stripKindSig t = t
 
 synifyInstHead :: ([TyVar], [PredType], Class, [Type]) -> InstHead GhcRn
-synifyInstHead (_, preds, cls, types) = specializeInstHead $ InstHead
+synifyInstHead (vs, preds, cls, types) = specializeInstHead $ InstHead
     { ihdClsName = getName cls
     , ihdTypes = map unLoc annot_ts
     , ihdInstType = ClassInst
-        { clsiCtx = map (unLoc . synifyType WithinType) preds
+        { clsiCtx = map (unLoc . synifyType WithinType []) preds
         , clsiTyVars = synifyTyVars (tyConVisibleTyVars cls_tycon)
         , clsiSigs = map synifyClsIdSig $ classMethods cls
         , clsiAssocTys = do
-            (Right (FamDecl _ fam)) <- map (synifyTyCon Nothing) $ classATs cls
+            (Right (FamDecl _ fam)) <- map (synifyTyCon HideRuntimeRep Nothing)
+                                           (classATs cls)
             pure $ mkPseudoFamilyDecl fam
         }
     }
   where
     cls_tycon = classTyCon cls
     ts  = filterOutInvisibleTypes cls_tycon types
-    ts' = map (synifyType WithinType) ts
+    ts' = map (synifyType WithinType vs) ts
     annot_ts = zipWith3 annotHsType is_poly_tvs ts ts'
     is_poly_tvs = mkIsPolyTvs (tyConVisibleTyVars cls_tycon)
-    synifyClsIdSig = synifyIdSig DeleteTopLevelQuantification
+    synifyClsIdSig = synifyIdSig ShowRuntimeRep DeleteTopLevelQuantification vs
 
 -- Convert a family instance, this could be a type family or data family
 synifyFamInst :: FamInst -> Bool -> Either ErrMsg (InstHead GhcRn)
@@ -623,9 +802,9 @@ synifyFamInst fi opaque = do
   where
     ityp SynFamilyInst | opaque = return $ TypeInst Nothing
     ityp SynFamilyInst =
-        return . TypeInst . Just . unLoc $ synifyType WithinType fam_rhs
+        return . TypeInst . Just . unLoc $ synifyType WithinType [] fam_rhs
     ityp (DataFamilyInst c) =
-        DataInst <$> synifyTyCon (Just $ famInstAxiom fi) c
+        DataInst <$> synifyTyCon HideRuntimeRep (Just $ famInstAxiom fi) c
     fam_tc     = famInstTyCon fi
     fam_flavor = fi_flavor fi
     fam_lhs    = fi_tys fi
@@ -645,7 +824,7 @@ synifyFamInst fi opaque = do
       = fam_lhs
 
     ts = filterOutInvisibleTypes fam_tc eta_expanded_lhs
-    synifyTypes = map (synifyType WithinType)
+    synifyTypes = map (synifyType WithinType [])
     ts' = synifyTypes ts
     annot_ts = zipWith3 annotHsType is_poly_tvs ts ts'
     is_poly_tvs = mkIsPolyTvs (tyConVisibleTyVars fam_tc)