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

11 files changed, 472 insertions, 240 deletions

diff --git a/haddock-api/src/Haddock/Backends/Hoogle.hs b/haddock-api/src/Haddock/Backends/Hoogle.hs
index 16ec582e..9e3186e5 100644
--- a/haddock-api/src/Haddock/Backends/Hoogle.hs
+++ b/haddock-api/src/Haddock/Backends/Hoogle.hs
@@ -263,8 +263,13 @@ ppCtor dflags dat subdocs con@ConDeclH98 {}
         -- docs for con_names on why it is a list to begin with.
         name = commaSeparate dflags . map unL $ getConNames con
 
-        resType = apps $ map (reL . HsTyVar NoExt NotPromoted . reL) $
-                        (tcdName dat) : [hsTyVarName v | L _ v@(UserTyVar _ _) <- hsQTvExplicit $ tyClDeclTyVars dat]
+        tyVarArg (UserTyVar _ n) = HsTyVar NoExt NotPromoted n
+        tyVarArg (KindedTyVar _ n lty) = HsKindSig NoExt (reL (HsTyVar NoExt NotPromoted n)) lty
+        tyVarArg _ = panic "ppCtor"
+
+        resType = apps $ map reL $
+                        (HsTyVar NoExt NotPromoted (reL (tcdName dat))) :
+                        map (tyVarArg . unLoc) (hsQTvExplicit $ tyClDeclTyVars dat)
 
 ppCtor dflags _dat subdocs con@(ConDeclGADT { })
    = concatMap (lookupCon dflags subdocs) (getConNames con) ++ f
diff --git a/haddock-api/src/Haddock/Backends/LaTeX.hs b/haddock-api/src/Haddock/Backends/LaTeX.hs
index 12256a00..d0752506 100644
--- a/haddock-api/src/Haddock/Backends/LaTeX.hs
+++ b/haddock-api/src/Haddock/Backends/LaTeX.hs
@@ -960,7 +960,7 @@ ppContext cxt unicode = ppContextNoLocs (map unLoc cxt) unicode
 
 pp_hs_context :: [HsType DocNameI] -> Bool -> LaTeX
 pp_hs_context []  _       = empty
-pp_hs_context [p] unicode = ppType unicode p
+pp_hs_context [p] unicode = ppCtxType unicode p
 pp_hs_context cxt unicode = parenList (map (ppType unicode) cxt)
 
 
@@ -995,11 +995,11 @@ ppLType       unicode y = ppType unicode (unLoc y)
 ppLParendType unicode y = ppParendType unicode (unLoc y)
 ppLFunLhType  unicode y = ppFunLhType unicode (unLoc y)
 
-
-ppType, ppParendType, ppFunLhType :: Bool -> HsType DocNameI -> LaTeX
+ppType, ppParendType, ppFunLhType, ppCtxType :: Bool -> HsType DocNameI -> LaTeX
 ppType       unicode ty = ppr_mono_ty (reparenTypePrec PREC_TOP ty) unicode
 ppParendType unicode ty = ppr_mono_ty (reparenTypePrec PREC_TOP ty) unicode
 ppFunLhType  unicode ty = ppr_mono_ty (reparenTypePrec PREC_FUN ty) unicode
+ppCtxType    unicode ty = ppr_mono_ty (reparenTypePrec PREC_CTX ty) unicode
 
 ppLHsTypeArg :: Bool -> LHsTypeArg DocNameI -> LaTeX
 ppLHsTypeArg unicode (HsValArg ty) = ppLParendType unicode ty
@@ -1045,7 +1045,7 @@ ppr_mono_ty (HsTupleTy _ con tys) u = tupleParens con (map (ppLType u) tys)
 ppr_mono_ty (HsSumTy _ tys) u       = sumParens (map (ppLType u) tys)
 ppr_mono_ty (HsKindSig _ ty kind) u = parens (ppr_mono_lty ty u <+> dcolon u <+> ppLKind u kind)
 ppr_mono_ty (HsListTy _ ty)       u = brackets (ppr_mono_lty ty u)
-ppr_mono_ty (HsIParamTy _ (L _ n) ty) u = brackets (ppIPName n <+> dcolon u <+> ppr_mono_lty ty u)
+ppr_mono_ty (HsIParamTy _ (L _ n) ty) u = ppIPName n <+> dcolon u <+> ppr_mono_lty ty u
 ppr_mono_ty (HsSpliceTy {})     _ = error "ppr_mono_ty HsSpliceTy"
 ppr_mono_ty (HsRecTy {})        _ = text "{..}"
 ppr_mono_ty (XHsType (NHsCoreTy {}))  _ = error "ppr_mono_ty HsCoreTy"
@@ -1110,7 +1110,7 @@ ppVerbOccName :: OccName -> LaTeX
 ppVerbOccName = text . latexFilter . occNameString
 
 ppIPName :: HsIPName -> LaTeX
-ppIPName ip = text $ unpackFS $ hsIPNameFS ip
+ppIPName = text . ('?':) . unpackFS . hsIPNameFS
 
 ppOccName :: OccName -> LaTeX
 ppOccName = text . occNameString
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)
diff --git a/haddock-api/src/Haddock/GhcUtils.hs b/haddock-api/src/Haddock/GhcUtils.hs
index a342de00..58cdd860 100644
--- a/haddock-api/src/Haddock/GhcUtils.hs
+++ b/haddock-api/src/Haddock/GhcUtils.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE BangPatterns, FlexibleInstances, ViewPatterns #-}
+{-# LANGUAGE BangPatterns, StandaloneDeriving, FlexibleInstances, ViewPatterns #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
@@ -24,6 +24,7 @@ import Data.Char ( isSpace )
 import Haddock.Types( DocNameI )
 
 import Exception
+import FV
 import Outputable ( Outputable, panic, showPpr )
 import Name
 import NameSet
@@ -33,6 +34,12 @@ import GHC
 import Class
 import DynFlags
 import SrcLoc    ( advanceSrcLoc )
+import Var       ( VarBndr(..), TyVarBinder, tyVarKind, updateTyVarKind,
+                   isInvisibleArgFlag )
+import VarSet    ( VarSet, emptyVarSet )
+import VarEnv    ( TyVarEnv, extendVarEnv, elemVarEnv, emptyVarEnv )
+import TyCoRep   ( Type(..), isRuntimeRepVar )
+import TysWiredIn( liftedRepDataConTyCon )
 
 import           StringBuffer ( StringBuffer )
 import qualified StringBuffer             as S
@@ -549,3 +556,104 @@ tryCppLine !loc !buf = spanSpace (S.prevChar buf '\n' == '\n') loc buf
 
         (c   , b') -> spanCppLine (advanceSrcLoc l c) b'
 
+-------------------------------------------------------------------------------
+-- * Free variables of a 'Type'
+-------------------------------------------------------------------------------
+
+-- | Get free type variables in a 'Type' in their order of appearance.
+-- See [Ordering of implicit variables].
+orderedFVs
+  :: VarSet  -- ^ free variables to ignore 
+  -> [Type]  -- ^ types to traverse (in order) looking for free variables
+  -> [TyVar] -- ^ free type variables, in the order they appear in
+orderedFVs vs tys =
+  reverse . fst $ tyCoFVsOfTypes' tys (const True) vs ([], emptyVarSet)
+
+
+-- See the "Free variables of types and coercions" section in 'TyCoRep', or
+-- check out Note [Free variables of types]. The functions in this section
+-- don't output type variables in the order they first appear in in the 'Type'.
+--
+-- For example, 'tyCoVarsOfTypeList' reports an incorrect order for the type
+-- of 'const :: a -> b -> a':
+--
+-- >>> import Name 
+-- >>> import TyCoRep
+-- >>> import TysPrim
+-- >>> import Var
+-- >>> a = TyVarTy alphaTyVar
+-- >>> b = TyVarTy betaTyVar
+-- >>> constTy = mkFunTys [a, b] a
+-- >>> map (getOccString . tyVarName) (tyCoVarsOfTypeList constTy)
+-- ["b","a"]
+--
+-- However, we want to reuse the very optimized traversal machinery there, so
+-- so we make our own `tyCoFVsOfType'`, `tyCoFVsBndr'`, and `tyCoVarsOfTypes'`.
+-- All these do differently is traverse in a different order and ignore
+-- coercion variables.
+
+-- | Just like 'tyCoFVsOfType', but traverses type variables in reverse order
+-- of  appearance.
+tyCoFVsOfType' :: Type -> FV
+tyCoFVsOfType' (TyVarTy v)        a b c = (FV.unitFV v `unionFV` tyCoFVsOfType' (tyVarKind v)) a b c
+tyCoFVsOfType' (TyConApp _ tys)   a b c = tyCoFVsOfTypes' tys a b c
+tyCoFVsOfType' (LitTy {})         a b c = emptyFV a b c
+tyCoFVsOfType' (AppTy fun arg)    a b c = (tyCoFVsOfType' arg `unionFV` tyCoFVsOfType' fun) a b c
+tyCoFVsOfType' (FunTy arg res)    a b c = (tyCoFVsOfType' res `unionFV` tyCoFVsOfType' arg) a b c
+tyCoFVsOfType' (ForAllTy bndr ty) a b c = tyCoFVsBndr' bndr (tyCoFVsOfType' ty)  a b c
+tyCoFVsOfType' (CastTy ty _)      a b c = (tyCoFVsOfType' ty) a b c
+tyCoFVsOfType' (CoercionTy _ )    a b c = emptyFV a b c
+
+-- | Just like 'tyCoFVsOfTypes', but traverses type variables in reverse order
+-- of appearance.
+tyCoFVsOfTypes' :: [Type] -> FV
+tyCoFVsOfTypes' (ty:tys) fv_cand in_scope acc = (tyCoFVsOfTypes' tys `unionFV` tyCoFVsOfType' ty) fv_cand in_scope acc
+tyCoFVsOfTypes' []       fv_cand in_scope acc = emptyFV fv_cand in_scope acc
+
+-- | Just like 'tyCoFVsBndr', but traverses type variables in reverse order of
+-- appearance.
+tyCoFVsBndr' :: TyVarBinder -> FV -> FV
+tyCoFVsBndr' (Bndr tv _) fvs = FV.delFV tv fvs `unionFV` tyCoFVsOfType' (tyVarKind tv)
+
+
+-------------------------------------------------------------------------------
+-- * Defaulting RuntimeRep variables
+-------------------------------------------------------------------------------
+
+-- | Traverses the type, defaulting type variables of kind 'RuntimeRep' to
+-- 'LiftedType'. See 'defaultRuntimeRepVars' in IfaceType.hs the original such
+-- function working over `IfaceType`'s.
+defaultRuntimeRepVars :: Type -> Type
+defaultRuntimeRepVars = go emptyVarEnv
+  where
+    go :: TyVarEnv () -> Type -> Type
+    go subs (ForAllTy (Bndr var flg) ty)
+      | isRuntimeRepVar var
+      , isInvisibleArgFlag flg
+      = let subs' = extendVarEnv subs var ()
+        in go subs' ty
+      | otherwise
+      = ForAllTy (Bndr (updateTyVarKind (go subs) var) flg)
+                 (go subs ty)
+
+    go subs (TyVarTy tv)
+      | tv `elemVarEnv` subs
+      = TyConApp liftedRepDataConTyCon []
+      | otherwise
+      = TyVarTy (updateTyVarKind (go subs) tv)
+
+    go subs (TyConApp tc tc_args)
+      = TyConApp tc (map (go subs) tc_args)
+
+    go subs (FunTy arg res)
+      = FunTy (go subs arg) (go subs res)
+
+    go subs (AppTy t u)
+      = AppTy (go subs t) (go subs u)
+
+    go subs (CastTy x co)
+      = CastTy (go subs x) co
+
+    go _ ty@(LitTy {}) = ty
+    go _ ty@(CoercionTy {}) = ty
+
diff --git a/haddock-api/src/Haddock/Interface/Create.hs b/haddock-api/src/Haddock/Interface/Create.hs
index 36cfeaca..95245cb2 100644
--- a/haddock-api/src/Haddock/Interface/Create.hs
+++ b/haddock-api/src/Haddock/Interface/Create.hs
@@ -891,7 +891,7 @@ hiDecl dflags t = do
     Nothing -> do
       liftErrMsg $ tell ["Warning: Not found in environment: " ++ pretty dflags t]
       return Nothing
-    Just x -> case tyThingToLHsDecl x of
+    Just x -> case tyThingToLHsDecl ShowRuntimeRep x of
       Left m -> liftErrMsg (tell [bugWarn m]) >> return Nothing
       Right (m, t') -> liftErrMsg (tell $ map bugWarn m)
                       >> return (Just $ noLoc t')
diff --git a/hoogle-test/ref/Bug873/test.txt b/hoogle-test/ref/Bug873/test.txt
index 3c0e1870..68873317 100644
--- a/hoogle-test/ref/Bug873/test.txt
+++ b/hoogle-test/ref/Bug873/test.txt
@@ -21,7 +21,7 @@ module Bug873
 --   Note that <tt>(<a>$</a>)</tt> is levity-polymorphic in its result
 --   type, so that <tt>foo <a>$</a> True</tt> where <tt>foo :: Bool -&gt;
 --   Int#</tt> is well-typed.
-($) :: () => (a -> b) -> a -> b
+($) :: forall (r :: RuntimeRep) a (b :: TYPE r). (a -> b) -> a -> b
 infixr 0 $
 ($$) :: (a -> b) -> a -> b
 infixr 0 $$
diff --git a/html-test/ref/Bug548.html b/html-test/ref/Bug548.html
index cff64ca2..e040e603 100644
--- a/html-test/ref/Bug548.html
+++ b/html-test/ref/Bug548.html
@@ -148,7 +148,9 @@
 			><p class="src"
 			><a href="#"
 			  >from1</a
-			  > :: <a href="#" title="Bug548"
+			  > :: <span class="keyword"
+			  >forall</span
+			  > (a0 :: k). <a href="#" title="Bug548"
 			  >WrappedArrow</a
 			  > a b a0 -&gt; <a href="#" title="GHC.Generics"
 			  >Rep1</a
@@ -160,7 +162,9 @@
 			><p class="src"
 			><a href="#"
 			  >to1</a
-			  > :: <a href="#" title="GHC.Generics"
+			  > :: <span class="keyword"
+			  >forall</span
+			  > (a0 :: k). <a href="#" title="GHC.Generics"
 			  >Rep1</a
 			  > (<a href="#" title="Bug548"
 			  >WrappedArrow</a
diff --git a/html-test/ref/Instances.html b/html-test/ref/Instances.html
index 4f51f049..0cf0fc92 100644
--- a/html-test/ref/Instances.html
+++ b/html-test/ref/Instances.html
@@ -2038,8 +2038,6 @@
 			  >Int</a
 			  > c <a href="#" title="Data.Bool"
 			  >Bool</a
-			  > :: <a href="#" title="Data.Kind"
-			  >Type</a
 			  > <a href="#" class="selflink"
 			  >#</a
 			  ></p
@@ -2050,9 +2048,7 @@
 			  >Thud</a
 			  > <a href="#" title="Data.Int"
 			  >Int</a
-			  > c :: <a href="#" title="Data.Kind"
-			  >Type</a
-			  > <a href="#" class="selflink"
+			  > c <a href="#" class="selflink"
 			  >#</a
 			  ></p
 			></div
@@ -2112,9 +2108,7 @@
 			  >type</span
 			  > <a href="#" title="Instances"
 			  >Plugh</a
-			  > [a] c [b] :: <a href="#" title="Data.Kind"
-			  >Type</a
-			  > <a href="#" class="selflink"
+			  > [a] c [b] <a href="#" class="selflink"
 			  >#</a
 			  ></p
 			><p class="src"
@@ -2122,9 +2116,7 @@
 			  >data</span
 			  > <a href="#" title="Instances"
 			  >Thud</a
-			  > [a] c :: <a href="#" title="Data.Kind"
-			  >Type</a
-			  > <a href="#" class="selflink"
+			  > [a] c <a href="#" class="selflink"
 			  >#</a
 			  ></p
 			></div
diff --git a/html-test/ref/Operators.html b/html-test/ref/Operators.html
index 8c7746af..d0c42a08 100644
--- a/html-test/ref/Operators.html
+++ b/html-test/ref/Operators.html
@@ -96,9 +96,7 @@
 	      >pattern</span
 	      > <a href="#"
 	      >(:+)</a
-	      > :: <span class="keyword"
-	      >forall</span
-	      > a. a -&gt; a -&gt; [a]</li
+	      > :: a -&gt; a -&gt; [a]</li
 	    ><li class="src short"
 	    ><span class="keyword"
 	      >data</span
@@ -285,9 +283,7 @@
 	    >pattern</span
 	    > <a id="v::-43-" class="def"
 	    >(:+)</a
-	    > :: <span class="keyword"
-	    >forall</span
-	    > a. a -&gt; a -&gt; [a] <span class="fixity"
+	    > :: a -&gt; a -&gt; [a] <span class="fixity"
 	    >infixr 3</span
 	    ><span class="rightedge"
 	    ></span
@@ -529,4 +525,4 @@
     ></div
     ></body
   ></html
->
+>
\ No newline at end of file
diff --git a/html-test/ref/PatternSyns.html b/html-test/ref/PatternSyns.html
index af6d0210..6b4f8fda 100644
--- a/html-test/ref/PatternSyns.html
+++ b/html-test/ref/PatternSyns.html
@@ -68,9 +68,7 @@
 	      >pattern</span
 	      > <a href="#"
 	      >Foo</a
-	      > :: <span class="keyword"
-	      >forall</span
-	      > x. x -&gt; <a href="#" title="PatternSyns"
+	      > :: x -&gt; <a href="#" title="PatternSyns"
 	      >FooType</a
 	      > x</li
 	    ><li class="src short"
@@ -78,9 +76,7 @@
 	      >pattern</span
 	      > <a href="#"
 	      >Bar</a
-	      > :: <span class="keyword"
-	      >forall</span
-	      > x. x -&gt; <a href="#" title="PatternSyns"
+	      > :: x -&gt; <a href="#" title="PatternSyns"
 	      >FooType</a
 	      > (<a href="#" title="PatternSyns"
 	      >FooType</a
@@ -90,9 +86,7 @@
 	      >pattern</span
 	      > <a href="#"
 	      >(:&lt;-&gt;)</a
-	      > :: <span class="keyword"
-	      >forall</span
-	      > x x1. x -&gt; x1 -&gt; (<a href="#" title="PatternSyns"
+	      > :: x -&gt; x1 -&gt; (<a href="#" title="PatternSyns"
 	      >FooType</a
 	      > x, <a href="#" title="PatternSyns"
 	      >FooType</a
@@ -114,9 +108,7 @@
 	      >pattern</span
 	      > <a href="#"
 	      >Blub</a
-	      > :: () =&gt; <span class="keyword"
-	      >forall</span
-	      > x. <a href="#" title="Text.Show"
+	      > :: () =&gt; <a href="#" title="Text.Show"
 	      >Show</a
 	      > x =&gt; x -&gt; <a href="#" title="PatternSyns"
 	      >BlubType</a
@@ -134,9 +126,7 @@
 	      >pattern</span
 	      > <a href="#"
 	      >E</a
-	      > :: <span class="keyword"
-	      >forall</span
-	      > k a (b :: k). a <a href="#" title="PatternSyns"
+	      > :: a <a href="#" title="PatternSyns"
 	      >&gt;&lt;</a
 	      > b</li
 	    ><li class="src short"
@@ -189,9 +179,7 @@
 	    >pattern</span
 	    > <a id="v:Foo" class="def"
 	    >Foo</a
-	    > :: <span class="keyword"
-	    >forall</span
-	    > x. x -&gt; <a href="#" title="PatternSyns"
+	    > :: x -&gt; <a href="#" title="PatternSyns"
 	    >FooType</a
 	    > x <a href="#" class="selflink"
 	    >#</a
@@ -211,9 +199,7 @@
 	    >pattern</span
 	    > <a id="v:Bar" class="def"
 	    >Bar</a
-	    > :: <span class="keyword"
-	    >forall</span
-	    > x. x -&gt; <a href="#" title="PatternSyns"
+	    > :: x -&gt; <a href="#" title="PatternSyns"
 	    >FooType</a
 	    > (<a href="#" title="PatternSyns"
 	    >FooType</a
@@ -235,9 +221,7 @@
 	    >pattern</span
 	    > <a id="v::-60--45--62-" class="def"
 	    >(:&lt;-&gt;)</a
-	    > :: <span class="keyword"
-	    >forall</span
-	    > x x1. x -&gt; x1 -&gt; (<a href="#" title="PatternSyns"
+	    > :: x -&gt; x1 -&gt; (<a href="#" title="PatternSyns"
 	    >FooType</a
 	    > x, <a href="#" title="PatternSyns"
 	    >FooType</a
@@ -291,9 +275,7 @@
 	    >pattern</span
 	    > <a id="v:Blub" class="def"
 	    >Blub</a
-	    > :: () =&gt; <span class="keyword"
-	    >forall</span
-	    > x. <a href="#" title="Text.Show"
+	    > :: () =&gt; <a href="#" title="Text.Show"
 	    >Show</a
 	    > x =&gt; x -&gt; <a href="#" title="PatternSyns"
 	    >BlubType</a
@@ -347,9 +329,7 @@
 	    >pattern</span
 	    > <a id="v:E" class="def"
 	    >E</a
-	    > :: <span class="keyword"
-	    >forall</span
-	    > k a (b :: k). a <a href="#" title="PatternSyns"
+	    > :: a <a href="#" title="PatternSyns"
 	    >&gt;&lt;</a
 	    > b <a href="#" class="selflink"
 	    >#</a
@@ -388,4 +368,4 @@
     ></div
     ></body
   ></html
->
+>
\ No newline at end of file
diff --git a/html-test/ref/TypeFamilies.html b/html-test/ref/TypeFamilies.html
index 492b7ec1..8e1e7364 100644
--- a/html-test/ref/TypeFamilies.html
+++ b/html-test/ref/TypeFamilies.html
@@ -286,8 +286,6 @@
 			  >AssocD</a
 			  > <a href="#" title="TypeFamilies"
 			  >X</a
-			  > :: <a href="#" title="Data.Kind"
-			  >Type</a
 			  > <a href="#" class="selflink"
 			  >#</a
 			  ></p
@@ -298,8 +296,6 @@
 			  >AssocT</a
 			  > <a href="#" title="TypeFamilies"
 			  >X</a
-			  > :: <a href="#" title="Data.Kind"
-			  >Type</a
 			  > <a href="#" class="selflink"
 			  >#</a
 			  ></p
@@ -720,8 +716,6 @@
 			  >AssocD</a
 			  > <a href="#" title="TypeFamilies"
 			  >Y</a
-			  > :: <a href="#" title="Data.Kind"
-			  >Type</a
 			  > <a href="#" class="selflink"
 			  >#</a
 			  ></p
@@ -732,8 +726,6 @@
 			  >AssocT</a
 			  > <a href="#" title="TypeFamilies"
 			  >Y</a
-			  > :: <a href="#" title="Data.Kind"
-			  >Type</a
 			  > <a href="#" class="selflink"
 			  >#</a
 			  ></p
@@ -1107,11 +1099,7 @@
 			><li class="inst"
 			  ><a id="v:BatZ1" class="def"
 			    >BatZ1</a
-			    > :: <span class="keyword"
-			    >forall</span
-			    > (z :: <a href="#" title="TypeFamilies"
-			    >Z</a
-			    >). <a href="#" title="TypeFamilies"
+			    > :: <a href="#" title="TypeFamilies"
 			    >Z</a
 			    > -&gt; <a href="#" title="TypeFamilies"
 			    >Bat</a
@@ -1121,11 +1109,7 @@
 			  ><li class="inst"
 			  ><a id="v:BatZ2" class="def"
 			    >BatZ2</a
-			    > :: <span class="keyword"
-			    >forall</span
-			    > (z :: <a href="#" title="TypeFamilies"
-			    >Z</a
-			    >). {..} -&gt; <a href="#" title="TypeFamilies"
+			    > :: {..} -&gt; <a href="#" title="TypeFamilies"
 			    >Bat</a
 			    > '<a href="#" title="TypeFamilies"
 			    >ZB</a
@@ -1393,11 +1377,7 @@
 			><li class="inst"
 			  ><a id="v:BatZ1" class="def"
 			    >BatZ1</a
-			    > :: <span class="keyword"
-			    >forall</span
-			    > (z :: <a href="#" title="TypeFamilies"
-			    >Z</a
-			    >). <a href="#" title="TypeFamilies"
+			    > :: <a href="#" title="TypeFamilies"
 			    >Z</a
 			    > -&gt; <a href="#" title="TypeFamilies"
 			    >Bat</a
@@ -1407,11 +1387,7 @@
 			  ><li class="inst"
 			  ><a id="v:BatZ2" class="def"
 			    >BatZ2</a
-			    > :: <span class="keyword"
-			    >forall</span
-			    > (z :: <a href="#" title="TypeFamilies"
-			    >Z</a
-			    >). {..} -&gt; <a href="#" title="TypeFamilies"
+			    > :: {..} -&gt; <a href="#" title="TypeFamilies"
 			    >Bat</a
 			    > '<a href="#" title="TypeFamilies"
 			    >ZB</a
@@ -1620,8 +1596,6 @@
 			  >AssocD</a
 			  > <a href="#" title="TypeFamilies"
 			  >Y</a
-			  > :: <a href="#" title="Data.Kind"
-			  >Type</a
 			  > <a href="#" class="selflink"
 			  >#</a
 			  ></p
@@ -1632,8 +1606,6 @@
 			  >AssocT</a
 			  > <a href="#" title="TypeFamilies"
 			  >Y</a
-			  > :: <a href="#" title="Data.Kind"
-			  >Type</a
 			  > <a href="#" class="selflink"
 			  >#</a
 			  ></p
@@ -1678,8 +1650,6 @@
 			  >AssocD</a
 			  > <a href="#" title="TypeFamilies"
 			  >X</a
-			  > :: <a href="#" title="Data.Kind"
-			  >Type</a
 			  > <a href="#" class="selflink"
 			  >#</a
 			  ></p
@@ -1690,8 +1660,6 @@
 			  >AssocT</a
 			  > <a href="#" title="TypeFamilies"
 			  >X</a
-			  > :: <a href="#" title="Data.Kind"
-			  >Type</a
 			  > <a href="#" class="selflink"
 			  >#</a
 			  ></p