Never generate a `tyvar <~ sigma` constraint

This patch changes the generation and canonicalization of <~
constraints, as shown in the document in docs/types.

Now, `tyvar <~ sigma` or `tyfam <~ sigma` constraint are not
regarded as canonical, and are converted to equalities at
canonicalisation time. However, care is taken to not generate
those equalities, neither in other canonicalisation steps or
in the constraint generation process.

This changes allows us to get rid of the `tct_flavor` flag
in `TyThing`, which remembered whether certain type was
coming from an un-annotated lamda or let. Now, since these
constructs get a new fresh variable, the desired constraint
with equality is to be generated.

17 files changed, 284 insertions, 286 deletions

diff --git a/compiler/coreSyn/CoreSubst.hs b/compiler/coreSyn/CoreSubst.hs
index 6fec2cf5f3..7465447aca 100644
--- a/compiler/coreSyn/CoreSubst.hs
+++ b/compiler/coreSyn/CoreSubst.hs
@@ -866,16 +866,9 @@ simpleOptExpr expr
         -- It's a bit painful to call exprFreeVars, because it makes
         -- three passes instead of two (occ-anal, and go)
 
-simplePassesOfSimplification :: Int
-simplePassesOfSimplification = 3
-
 simpleOptExprWith :: Subst -> InExpr -> OutExpr
 -- Make three passes of simplification
-simpleOptExprWith subst expr
-  = iterate (simpleOptExprWith_ subst) expr !! simplePassesOfSimplification
-
-simpleOptExprWith_ :: Subst -> InExpr -> OutExpr
-simpleOptExprWith_ subst expr = simple_opt_expr subst (occurAnalyseExpr expr)
+simpleOptExprWith subst expr = simple_opt_expr subst (occurAnalyseExpr expr)
 
 ----------------------
 simpleOptPgm :: DynFlags -> Module
@@ -892,7 +885,7 @@ simpleOptPgm dflags this_mod binds rules vects
     (subst', binds') = foldl do_one (emptySubst, []) occ_anald_binds
 
     do_one (subst, binds') bind
-      = case simple_opt_bind_pgm subst bind of
+      = case simple_opt_bind subst bind of
           (subst', Nothing)    -> (subst', binds')
           (subst', Just bind') -> (subst', bind':binds')
 
@@ -992,16 +985,12 @@ simple_app subst e as
   = foldl App (simple_opt_expr subst e) as
 
 ----------------------
-simple_opt_bind,simple_opt_bind',simple_opt_bind_pgm
+simple_opt_bind,simple_opt_bind'
   :: Subst -> CoreBind -> (Subst, Maybe CoreBind)
 simple_opt_bind s b               -- Can add trace stuff here
   = simple_opt_bind' s b
 
-simple_opt_bind'    = simple_opt_bind'' 1
-simple_opt_bind_pgm = simple_opt_bind'' simplePassesOfSimplification
-
-simple_opt_bind'' :: Int -> Subst -> CoreBind -> (Subst, Maybe CoreBind)
-simple_opt_bind'' simpl_passes subst (Rec prs)
+simple_opt_bind' subst (Rec prs)
   = (subst'', res_bind)
   where
     res_bind            = Just (Rec (reverse rev_prs'))
@@ -1013,10 +1002,10 @@ simple_opt_bind'' simpl_passes subst (Rec prs)
            Nothing     -> (subst,  (b2,r2):prs)
        where
          b2 = add_info subst b b'
-         r2 = iterate (simple_opt_expr subst) r !! simpl_passes
+         r2 = simple_opt_expr subst r
 
-simple_opt_bind'' simpl_passes subst (NonRec b r)
-  = simple_opt_out_bind subst (b, iterate (simple_opt_expr subst) r !! simpl_passes)
+simple_opt_bind' subst (NonRec b r)
+  = simple_opt_out_bind subst (b, simple_opt_expr subst r)
 
 ----------------------
 simple_opt_out_bind :: Subst -> (InVar, OutExpr) -> (Subst, Maybe CoreBind)
diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs
index 04df777931..b7d6421681 100644
--- a/compiler/deSugar/DsBinds.hs
+++ b/compiler/deSugar/DsBinds.hs
@@ -1187,18 +1187,19 @@ applyInstanceOf id e
   = pprPanic "The impossible happened" (ppr id)
 
 dsEvInstanceOf :: EvInstanceOf -> CoreExpr -> DsM CoreExpr
-dsEvInstanceOf EvInstanceOfRefl e
-  = return e
-dsEvInstanceOf (EvInstanceOfEq co) e
-  = do { dsTcCoercion co $ \c ->
-           case coercionKind c of
-             Pair ty1 ty2 | ty1 == ty2 -> e  -- No conversion needed
-             _ ->  mkCast e (mkSubCo c) }
 dsEvInstanceOf (EvInstanceOfInst qvars co qs) e
   = do { qs' <- mapM dsEvTerm qs
        ; let exprTy = mkCoreApps e (map Type qvars)
              exprEv = mkCoreApps exprTy qs'
        ; return $ applyInstanceOf co exprEv }
+dsEvInstanceOf (EvInstanceOfInstEq qvars co qs) e
+  = do { qs' <- mapM dsEvTerm qs
+       ; let exprTy = mkCoreApps e (map Type qvars)
+             exprEv = mkCoreApps exprTy qs'
+       ; dsTcCoercion co $ \c ->
+           case coercionKind c of
+             Pair ty1 ty2 | ty1 == ty2 -> exprEv
+             _ -> mkCast exprEv (mkSubCo c) }
 dsEvInstanceOf (EvInstanceOfGen tyvars qvars qs rest) e
   = do { q_binds <- dsTcEvBinds qs
        ; return $ mkCoreLams (tyvars ++ qvars)
diff --git a/compiler/typecheck/TcArrows.hs b/compiler/typecheck/TcArrows.hs
index 7b61d67927..c30f9e0522 100644
--- a/compiler/typecheck/TcArrows.hs
+++ b/compiler/typecheck/TcArrows.hs
@@ -361,8 +361,7 @@ tcArrDoStmt env ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names
   = do  { let tup_names = rec_names ++ filterOut (`elem` rec_names) later_names
         ; tup_elt_tys <- newFlexiTyVarTys (length tup_names) liftedTypeKind
         ; let tup_ids  = zipWith mkLocalId tup_names tup_elt_tys
-              tup_ids' = [(tup_id, TcIdMonomorphic) | tup_id <- tup_ids]
-        ; tcExtendIdEnv tup_ids' $ do
+        ; tcExtendIdEnv tup_ids $ do
         { (stmts', tup_rets)
                 <- tcStmtsAndThen ctxt (tcArrDoStmt env) stmts res_ty   $ \ _res_ty' ->
                         -- ToDo: res_ty not really right
diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index c206804c92..e26611a6da 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -371,7 +371,7 @@ tcValBinds top_lvl binds sigs thing_inside
                 -- declared with complete type signatures
                 -- Do not extend the TcIdBinderStack; instead
                 -- we extend it on a per-rhs basis in tcExtendForRhs
-        ; tcExtendLetEnvIds top_lvl [(idName id, id, choose_tc_id_flavor id) | id <- poly_ids] $ do
+        ; tcExtendLetEnvIds top_lvl [(idName id, id) | id <- poly_ids] $ do
             { (binds', (extra_binds', thing)) <- tcBindGroups top_lvl sig_fn prag_fn binds $ do
                    { thing <- thing_inside
                      -- See Note [Pattern synonym builders don't yield dependencies]
@@ -447,8 +447,7 @@ tc_group top_lvl sig_fn prag_fn (Recursive, binds) thing_inside
 
     go :: [SCC (LHsBind Name)] -> TcM (LHsBinds TcId, thing)
     go (scc:sccs) = do  { (binds1, ids1) <- tc_scc scc
-                        ; let uids1 = map (\x -> (x, choose_tc_id_flavor x)) ids1
-                        ; (binds2, thing) <- tcExtendLetEnv top_lvl uids1 $
+                        ; (binds2, thing) <- tcExtendLetEnv top_lvl ids1 $
                                              go sccs
                         ; return (binds1 `unionBags` binds2, thing) }
     go []         = do  { thing <- thing_inside; return (emptyBag, thing) }
@@ -488,15 +487,9 @@ tc_single top_lvl sig_fn prag_fn lbind thing_inside
   = do { (binds1, ids) <- tcPolyBinds top_lvl sig_fn prag_fn
                                       NonRecursive NonRecursive
                                       [lbind]
-       ; let uids = map (\x -> (x, choose_tc_id_flavor x)) ids
-       ; thing <- tcExtendLetEnv top_lvl uids thing_inside
+       ; thing <- tcExtendLetEnv top_lvl ids thing_inside
        ; return (binds1, thing) }
 
-choose_tc_id_flavor :: Id -> TcIdFlavor
-choose_tc_id_flavor v
-  | Just _ <- tcGetTyVar_maybe (idType v) = TcIdMonomorphic
-  | otherwise = TcIdUnrestricted
-
 -- | No signature or a partial signature
 noCompleteSig :: Maybe TcSigInfo -> Bool
 noCompleteSig Nothing    = True
@@ -1363,14 +1356,14 @@ tcMonoBinds _ sig_fn no_gen binds
 
         -- Bring the monomorphic Ids, into scope for the RHSs
         ; let mono_info  = getMonoBindInfo tc_binds
-              rhs_id_env = [(name, mono_id, choose_tc_id_flavor mono_id)
+              rhs_id_env = [(name, mono_id)
                            | (name, mb_sig, mono_id) <- mono_info
                            , noCompleteSig mb_sig ]
                     -- A monomorphic binding for each term variable that lacks
                     -- a type sig.  (Ones with a sig are already in scope.)
 
         ; traceTc "tcMonoBinds" $ vcat [ ppr n <+> ppr id <+> ppr (idType id)
-                                       | (n,id,_) <- rhs_id_env]
+                                       | (n,id) <- rhs_id_env]
         ; binds' <- tcExtendLetEnvIds NotTopLevel rhs_id_env $
                     mapM (wrapLocM tcRhs) tc_binds
         ; return (listToBag binds', mono_info) }
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index f5959d485d..50f6cf0a43 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1679,8 +1679,8 @@ canInstanceOfNC ev
 canInstanceOf :: CtEvidence -> TcS (StopOrContinue Ct)
 canInstanceOf ev
   = do { let Just (tc, [lhs, rhs]) = splitTyConApp_maybe (ctEvPred ev)
-       ; (xil, col) <- flatten FM_SubstOnly ev lhs
-       ; (xir, cor) <- flatten FM_SubstOnly ev rhs
+       ; (xil, col) <- flatten FM_FlattenAll ev lhs
+       ; (xir, cor) <- flatten FM_FlattenAll ev rhs
        ; let co = mkTcTyConAppCo Nominal tc [col, cor]
              xi = mkInstanceOfPred xil xir
              mk_ct new_ev = CInstanceOfCan { cc_ev = new_ev
@@ -1693,39 +1693,31 @@ can_instance_of :: Ct -> TcS (StopOrContinue Ct)
 can_instance_of (CInstanceOfCan { cc_ev = ev, cc_lhs = lhs, cc_rhs = rhs })
     -- case InstanceOf sigma sigma, for the exact same sigma
   | lhs `eqType` rhs
-  = case ev of
-      CtWanted { ctev_evar = evar } ->
-        do { setWantedEvBind evar (mkInstanceOfRefl lhs)
-           ; stopWith ev "can_instance_of/REFL" }
-      _ -> stopWith ev "Given/Derived instanceOf instantiation"
+  = can_instance_to_eq ev lhs rhs
     -- case InstanceOf ty (forall qvars. Q => ty)
-  | is_forall rhs
+    -- rule [<~Rforall]
+  | isSigmaTy rhs
   = case ev of
       CtWanted { ctev_evar = evar, ctev_loc = loc } ->
         do { ev_let <- deferTcSForAllInstanceOf loc lhs rhs
            ; setWantedEvBind evar ev_let
            ; stopWith ev "can_instance_of/LET" }
       _ -> stopWith ev "Given/Derived instanceOf instantiation"
-    -- case InstanceOf (forall qvars. Q => ty) sigma
-    -- where sigma is T ... or a Skolem tyvar
-  | is_forall lhs, not (is_mutable_tyvar rhs)
+    -- case InstanceOf (forall qvars. Q => sigma) psi
+    -- rules [<~LforallpsiRpsi] and [<~LforallupsilonRpsi]
+  | isSigmaTy lhs, not (isSigmaTy rhs), not (isUpsilonTy rhs)
   = can_instance_inst ev lhs rhs
-    -- case InstanceOf (T ...) sigma --> T ... ~ sigma
-    -- case InstanceOf var sigma --> var ~ sigma, var immutable
-  | not (is_forall lhs)  -- is_tyapp_or_skolem lhs
+    -- case InstanceOf (forall qvars. upsilon) upsilon
+    -- rule [<~LforallupsilonRupsilon]
+  | (_:_, [], ty) <- tcSplitSigmaTy lhs, isUpsilonTy ty
+  , isUpsilonTy rhs
+  = can_instance_inst ev lhs rhs
+    -- case InstanceOf tau tau --> tau ~ tau
+    -- rule [<~LtauRtau]
+  | not (isSigmaTy lhs) --, not (is_forall rhs)
   = can_instance_to_eq ev lhs rhs
     -- already canonical
   | otherwise = continueWith (CIrredEvCan { cc_ev = ev })
-  where
-    is_forall ty
-      | ([], [], _) <- tcSplitSigmaTy ty = False
-      | otherwise                        = True
-
-    is_mutable_tyvar ty
-      | Just v <- getTyVar_maybe ty
-      = not (isImmutableTyVar v)
-      | otherwise
-      = False
 
 can_instance_of _ = panic "can_instance_of in a non instanceOf constraint"
 
@@ -1749,14 +1741,22 @@ can_instance_inst ev lhs rhs
       do { (qvars, q, ty) <- splitInst lhs
            -- generate new constraints
          ; new_ev_qs <- mapM (newWantedEvVarNC loc) q
-         ; let inst = mkInstanceOfPred ty rhs
-         ; new_ev_inst <- newWantedEvVarNC loc inst
-           -- compute the evidence for the instantiation
          ; let qvars' = map mkTyVarTy qvars
-         ; setWantedEvBind evar (mkInstanceOfInst lhs qvars' (ctEvId new_ev_inst)
-                                                  (map ctev_evar new_ev_qs))
-           -- emit new work
-         ; emitWorkNC new_ev_qs
-         ; traceTcS "can_instance_of/INST" (vcat [ ppr new_ev_inst, ppr new_ev_qs ])
-         ; canInstanceOfNC new_ev_inst }
+               evars' = map ctev_evar new_ev_qs
+         ; if isUpsilonTy ty
+           then do { let inst = mkInstanceOfPred ty rhs
+                   ; new_ev_inst <- newWantedEvVarNC loc inst
+                   ; setWantedEvBind evar
+                       (mkInstanceOfInst lhs qvars' (ctEvId new_ev_inst) evars')
+                   ; emitWorkNC new_ev_qs
+                   ; traceTcS "can_instance_of/INST" (vcat [ ppr new_ev_inst, ppr new_ev_qs ])
+                   ; canInstanceOfNC new_ev_inst }
+                -- if the inner type is upsilon, generate equality
+           else do { let eq = mkTcEqPredRole Nominal ty rhs
+                   ; new_ev_eq <- newWantedEvVarNC loc eq
+                   ; setWantedEvBind evar
+                       (mkInstanceOfInstEq lhs qvars' (ctEvCoercion new_ev_eq) evars')
+                   ; emitWorkNC new_ev_qs
+                   ; traceTcS "can_instance_of/INSTEQ" (vcat [ ppr new_ev_eq, ppr new_ev_qs ])
+                   ; canEqNC new_ev_eq NomEq ty rhs } }
     _ -> stopWith ev "Given/Derived instanceOf instantiation"
diff --git a/compiler/typecheck/TcEnv.hs b/compiler/typecheck/TcEnv.hs
index ab51f5eec4..b4635af6c1 100644
--- a/compiler/typecheck/TcEnv.hs
+++ b/compiler/typecheck/TcEnv.hs
@@ -404,43 +404,41 @@ isClosedLetBndr id
   | isEmptyVarSet (tyVarsOfType (idType id)) = TopLevel
   | otherwise                                = NotTopLevel
 
-tcExtendLetEnv :: TopLevelFlag -> [(TcId, TcIdFlavor)] -> TcM a -> TcM a
+tcExtendLetEnv :: TopLevelFlag -> [TcId] -> TcM a -> TcM a
 -- Used for both top-level value bindings and and nested let/where-bindings
 -- Adds to the TcIdBinderStack too
 tcExtendLetEnv top_lvl ids thing_inside
-  = tcExtendIdBndrs [TcIdBndr id top_lvl | (id, _) <- ids] $
-    tcExtendLetEnvIds top_lvl [(idName id, id, flavor) | (id, flavor) <- ids] thing_inside
+  = tcExtendIdBndrs [TcIdBndr id top_lvl | id <- ids] $
+    tcExtendLetEnvIds top_lvl [(idName id, id) | id <- ids] thing_inside
 
-tcExtendLetEnvIds :: TopLevelFlag -> [(Name,TcId,TcIdFlavor)] -> TcM a -> TcM a
+tcExtendLetEnvIds :: TopLevelFlag -> [(Name,TcId)] -> TcM a -> TcM a
 -- Used for both top-level value bindings and and nested let/where-bindings
 -- Does not extend the TcIdBinderStack
 tcExtendLetEnvIds top_lvl pairs thing_inside
   = tc_extend_local_env top_lvl [ (name, ATcId { tct_id = id
-                                               , tct_closed = isClosedLetBndr id
-                                               , tct_flavor = flavor })
-                                | (name,id,flavor) <- pairs ] $
+                                               , tct_closed = isClosedLetBndr id })
+                                | (name, id) <- pairs ] $
     thing_inside
 
-tcExtendIdEnv :: [(TcId, TcIdFlavor)] -> TcM a -> TcM a
+tcExtendIdEnv :: [(TcId)] -> TcM a -> TcM a
 -- For lambda-bound and case-bound Ids
 -- Extends the the TcIdBinderStack as well
 tcExtendIdEnv ids thing_inside
-  = tcExtendIdEnv2 [(idName id, id, flavor) | (id, flavor) <- ids] thing_inside
+  = tcExtendIdEnv2 [(idName id, id) | id <- ids] thing_inside
 
-tcExtendIdEnv1 :: Name -> TcId -> TcIdFlavor -> TcM a -> TcM a
+tcExtendIdEnv1 :: Name -> TcId -> TcM a -> TcM a
 -- Exactly like tcExtendIdEnv2, but for a single (name,id) pair
-tcExtendIdEnv1 name id flavor thing_inside
-  = tcExtendIdEnv2 [(name,id,flavor)] thing_inside
+tcExtendIdEnv1 name id thing_inside
+  = tcExtendIdEnv2 [(name, id)] thing_inside
 
-tcExtendIdEnv2 :: [(Name,TcId,TcIdFlavor)] -> TcM a -> TcM a
+tcExtendIdEnv2 :: [(Name,TcId)] -> TcM a -> TcM a
 tcExtendIdEnv2 names_w_ids thing_inside
   = tcExtendIdBndrs [ TcIdBndr mono_id NotTopLevel
-                    | (_,mono_id,_) <- names_w_ids ] $
+                    | (_, mono_id) <- names_w_ids ] $
     do  { tc_extend_local_env NotTopLevel
                               [ (name, ATcId { tct_id = id
-                                             , tct_closed = NotTopLevel
-                                             , tct_flavor = flavor })
-                              | (name,id,flavor) <- names_w_ids] $
+                                             , tct_closed = NotTopLevel })
+                              | (name, id) <- names_w_ids] $
           thing_inside }
 
 tc_extend_local_env :: TopLevelFlag -> [(Name, TcTyThing)]
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index 9b4d132505..81ba9cc3d0 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -18,8 +18,8 @@ module TcEvidence (
   EvLit(..), evTermCoercion,
   EvCallStack(..),
   EvTypeable(..),
-  EvInstanceOf(..), mkInstanceOfRefl, mkInstanceOfEq,
-  mkInstanceOfInst, mkInstanceOfGen,
+  EvInstanceOf(..),
+  mkInstanceOfEq, mkInstanceOfInst, mkInstanceOfInstEq, mkInstanceOfGen,
 
   -- TcCoercion
   TcCoercion(..), TcCoercionR, TcCoercionN,
@@ -781,10 +781,6 @@ data EvCallStack
 {- Note [Evidence for InstanceOf constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-             g : t ~N t
-    --------------------------
-    EvInstanceOfRefl : t <~ t
-
              g : s ~N t
     --------------------------
     EvInstanceOfEq g : s <~ t
@@ -793,20 +789,24 @@ data EvCallStack
     -------------------------------------------------------------------------
     EvInstanceOfInst [t1..tm] g [v1..vn] : (forall a1..am., c1..ck => s) <~ t
 
+                 g : (s[tys/as] ~ t),   vi : ci[tys/as]
+    ---------------------------------------------------------------------------
+    EvInstanceOfInstEq [t1..tm] g [v1..vn] : (forall a1..am., c1..ck => s) <~ t
+
                  forall [a1..an]. [v1:c1,..vn:cn] <binds>. g : s <~ t
     -------------------------------------------------------------------------
     EvInstanceOfGen [a1..an] [v1..vn] <binds> g : s <~ (forall a1..am., c1..ck => t)
 -}
 
 data EvInstanceOf
-  = EvInstanceOfRefl
-
-  | EvInstanceOfEq   TcCoercion  -- ^ term witnessing equality
-
-  | EvInstanceOfInst [Type]      -- ^ type variables to apply
+  = EvInstanceOfInst [Type]      -- ^ type variables to apply
                      EvId        -- ^ witness for inner instantiation
                      [EvTerm]    -- ^ witness for inner constraints
 
+  | EvInstanceOfInstEq [Type]
+                       TcCoercion
+                       [EvTerm]
+
   | EvInstanceOfGen  [TyVar]     -- ^ type variables
                      [EvId]      -- ^ constraint variables
                      TcEvBinds   -- ^ inner bindings
@@ -814,18 +814,18 @@ data EvInstanceOf
 
     deriving ( Data.Data, Data.Typeable )
 
-mkInstanceOfRefl :: Type -> EvTerm
-mkInstanceOfRefl ty
-  = EvInstanceOf ty EvInstanceOfRefl
-
 mkInstanceOfEq :: Type -> TcCoercion -> EvTerm
 mkInstanceOfEq ty co
-  = EvInstanceOf ty (EvInstanceOfEq co)
+  = mkInstanceOfInstEq ty [] co []
 
 mkInstanceOfInst :: Type -> [Type] -> EvId -> [EvVar] -> EvTerm
 mkInstanceOfInst ty vars co q
   = EvInstanceOf ty (EvInstanceOfInst vars co (map EvId q))
 
+mkInstanceOfInstEq :: Type -> [Type] -> TcCoercion -> [EvVar] -> EvTerm
+mkInstanceOfInstEq ty vars co q
+  = EvInstanceOf ty (EvInstanceOfInstEq vars co (map EvId q))
+
 mkInstanceOfGen :: Type -> [TyVar] -> [EvId] -> TcEvBinds -> EvId -> EvTerm
 mkInstanceOfGen ty tyvars qvars bnds co
   = EvInstanceOf ty (EvInstanceOfGen tyvars qvars bnds co)
@@ -1093,9 +1093,8 @@ evVarsOfTypeable ev =
 evVarsOfInstanceOf :: EvInstanceOf -> VarSet
 evVarsOfInstanceOf ev =
   case ev of
-    EvInstanceOfRefl        -> emptyVarSet
-    EvInstanceOfEq   co     -> coVarsOfTcCo co
-    EvInstanceOfInst _ co q -> unitVarSet co `unionVarSet` evVarsOfTerms q
+    EvInstanceOfInst   _ co q -> unitVarSet co `unionVarSet` evVarsOfTerms q
+    EvInstanceOfInstEq _ co q -> coVarsOfTcCo co `unionVarSet` evVarsOfTerms q
     EvInstanceOfGen  _ qvars (EvBinds bs) co ->
       (foldrBag (unionVarSet . go_bind) (unitVarSet co) bs
        `minusVarSet` get_bndrs bs) `minusVarSet` mkVarSet qvars
@@ -1197,10 +1196,10 @@ instance Outputable EvTypeable where
 instance Outputable EvInstanceOf where
   ppr ev =
     case ev of
-      EvInstanceOfRefl     -> ptext (sLit "REFL")
-      EvInstanceOfEq   co  -> ptext (sLit "EQ")   <+> ppr co
       EvInstanceOfInst vars co q
-        -> ptext (sLit "INST") <+> ppr vars <+> ppr q <+> ppr co
+        -> ptext (sLit "INST")   <+> ppr vars <+> ppr q <+> ppr co
+      EvInstanceOfInstEq vars co q
+        -> ptext (sLit "INSTEQ") <+> ppr vars <+> ppr q <+> ppr co
       EvInstanceOfGen  vars qvars b i
         -> ptext (sLit "LET") <+> ppr vars <+> ppr qvars
                               <+> ppr b <+> ppr i
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index 800d47836c..9b73562c44 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -485,7 +485,7 @@ tcExpr (RecordCon (L loc con_name) _ rbinds) res_ty
         ; checkMissingFields data_con rbinds
 
         -- Get type of the constructor
-        ; (con_expr, _, con_sigma) <- tcIdOcc (OccurrenceOf con_name) con_name
+        ; (con_expr, con_sigma) <- tcIdOcc (OccurrenceOf con_name) con_name
         ; (wrap, con_rho) <- instFunTy con_sigma  -- Eagerly instantiate
 
         ; let arity = dataConSourceArity data_con
@@ -945,7 +945,7 @@ tcAppWorker (L loc (HsVar fun_name)) args res_ty
   | fun_name `hasKey` dollarIdKey   -- Note [Typing rule for ($)]
   , ((L actual_loc (HsVar actual_fun_name)) : rest_args) <- args
   = do {   -- Typing without ($)
-         (fun_expr, _, fun_sigma) <- tcIdOcc (OccurrenceOf actual_fun_name) actual_fun_name
+         (fun_expr, fun_sigma) <- tcIdOcc (OccurrenceOf actual_fun_name) actual_fun_name
        ; (wrap, fun_rho) <- instFunTy fun_sigma   -- Eagerly instantiate
        ; result <- tc_app (L actual_loc (mkHsWrap wrap fun_expr)) rest_args fun_rho res_ty
 
@@ -956,7 +956,7 @@ tcAppWorker (L loc (HsVar fun_name)) args res_ty
 
   | otherwise  -- The common case: a variable other than '$', 'tagToEnum, or 'seq',
                --                  applied to a list of arguments
-  = do { (fun_expr, _, fun_sigma) <- tcIdOcc (OccurrenceOf fun_name) fun_name
+  = do { (fun_expr, fun_sigma) <- tcIdOcc (OccurrenceOf fun_name) fun_name
        ; (wrap, fun_rho) <- instFunTy fun_sigma   -- Eagerly instantiate
        ; tc_app (L loc (mkHsWrap wrap fun_expr)) args fun_rho res_ty }
 
@@ -1001,30 +1001,27 @@ tc_app fun_expr args fun_ty res_ty
         ; args1 <- tcArgs fun_expr args expected_arg_tys
 
         -- Both actual_res_ty and res_ty are deeply skolemised
-        -- Split in cases depending on whether res_ty is a variable or not
-        -- When it is, generate a equality constraint instead of instantiation
+        -- Never generate a upsilon <~ sigma constraint
         -- This is needed to compile some programs such as
         -- > data S a = S a
         -- > f :: [Char] -> S a
         -- > f x = S (error x)
         -- Without it, the `a` coming from `f` cannot be unified with
         -- the second type variable of `error`
-        ; case getTyVar_maybe actual_res_ty of
-          { Nothing
-              -> do { ev_res <- addErrCtxtM (funResCtxt True (unLoc fun_expr) actual_res_ty res_ty) $
-                                emitWanted AppOrigin (mkInstanceOfPred actual_res_ty res_ty)
-                    ; return $ TcAppResult
-                       (mkLHsWrapCo co_fun fun_expr)  -- Instantiated function
-                       args1                          -- Arguments
-                                                      -- Coercion to expected result type
-                       (mkWpInstanceOf ev_res) }
-          ; Just _
-              -> do { co_res <- addErrCtxtM (funResCtxt True (unLoc fun_expr) actual_res_ty res_ty) $
-                                unifyType actual_res_ty res_ty
-                    ; return $ TcAppResult
-                       (mkLHsWrapCo co_fun fun_expr)  -- Instantiated function
-                       args1                          -- Arguments
-                       (coToHsWrapper co_res) } } }   -- Coercion to expected result type
+        ; if isUpsilonTy actual_res_ty
+             then do { ev_res <- addErrCtxtM (funResCtxt True (unLoc fun_expr) actual_res_ty res_ty) $
+                                 emitWanted AppOrigin (mkInstanceOfPred actual_res_ty res_ty)
+                     ; return $ TcAppResult
+                        (mkLHsWrapCo co_fun fun_expr)  -- Instantiated function
+                        args1                          -- Arguments
+                                                       -- Coercion to expected result type
+                        (mkWpInstanceOf ev_res) }
+             else do { co_res <- addErrCtxtM (funResCtxt True (unLoc fun_expr) actual_res_ty res_ty) $
+                                 unifyType actual_res_ty res_ty
+                     ; return $ TcAppResult
+                        (mkLHsWrapCo co_fun fun_expr)  -- Instantiated function
+                        args1                          -- Arguments
+                        (coToHsWrapper co_res) } }     -- Coercion to expected result type
 
 mk_app_msg :: Outputable a => a -> SDoc
 mk_app_msg fun = sep [ ptext (sLit "The function") <+> quotes (ppr fun)
@@ -1163,43 +1160,40 @@ tc_infer_assert dflags orig
 tc_check_id :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId)
 -- Return type is deeply instantiated
 tc_check_id orig id_name res_ty
- = do { (id_expr, flavour, id_ty) <- tcIdOcc orig id_name
-      ; case flavour of
-          TcIdMonomorphic  -- Generate an equality constraint
-            -> do { co <- unifyType id_ty res_ty
-                  ; return (mkHsWrapCo co id_expr) }
-
-          TcIdUnrestricted  -- Generate an instance-of constraint
-                 -> do { ev <- emitWanted orig (mkInstanceOfPred id_ty res_ty)
-                       ; return (mkHsWrap (mkWpInstanceOf ev) id_expr) } }
-
-tcIdOcc :: CtOrigin -> Name -> TcM (HsExpr TcId, TcIdFlavor, TcSigmaType)
+ = do { (id_expr, id_ty) <- tcIdOcc orig id_name
+      ; if isUpsilonTy id_ty
+           then do { co <- unifyType id_ty res_ty
+                   ; return (mkHsWrapCo co id_expr) }
+           else do { ev <- emitWanted orig (mkInstanceOfPred id_ty res_ty)
+                   ; return (mkHsWrap (mkWpInstanceOf ev) id_expr) } }
+
+tcIdOcc :: CtOrigin -> Name -> TcM (HsExpr TcId, TcSigmaType)
 -- Check an occurrence of an Id in a term
 -- Do not instantiate it, except in the legacy case
 -- of data constructors with a stupid theta
 tcIdOcc orig name
   = do { thing <- tcLookup name
        ; case thing of
-             ATcId { tct_id = id, tct_flavor = flavor }
+             ATcId { tct_id = id }
                -> do { check_naughty id        -- Note [Local record selectors]
                      ; checkThLocalId id
-                     ; return (HsVar id, flavor, idType id) }
+                     ; return (HsVar id, idType id) }
 
              AGlobal (AnId id)
                -> do { check_naughty id
-                     ; return (HsVar id, TcIdUnrestricted, idType id) }
+                     ; return (HsVar id, idType id) }
                     -- A global cannot possibly be ill-staged
                     -- nor does it need the 'lifting' treatment
                     -- hence no checkTh stuff here
 
              AGlobal (AConLike (PatSynCon ps))
                -> do { (expr, res_ty) <- tcPatSynBuilderOcc orig ps
-                     ; return (expr, TcIdMonomorphic, res_ty) }
+                     ; return (expr, res_ty) }
                      -- ToDo: instantiate pattern synonyms lazily
 
              AGlobal (AConLike (RealDataCon con))
                | null (dataConStupidTheta con)
-               -> return (HsVar (dataConWrapId con), TcIdUnrestricted, idType (dataConWrapId con))
+               -> return (HsVar (dataConWrapId con), idType (dataConWrapId con))
                | otherwise  -- Legacy case: always instantiate eagerly
                -> inst_stupid_data_con con
 
@@ -1221,7 +1215,7 @@ tcIdOcc orig name
                  rho'   = substTy subst rho
            ; wrap <- instCall orig tys' theta'
            ; addDataConStupidTheta con tys'
-           ; return (mkHsWrap wrap (HsVar (dataConWrapId con)), TcIdMonomorphic, rho') }
+           ; return (mkHsWrap wrap (HsVar (dataConWrapId con)), rho') }
 
 
 srcSpanPrimLit :: DynFlags -> SrcSpan -> HsExpr TcId
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 9ca25b75ae..8cb50039b2 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -1328,16 +1328,16 @@ zonkEvBind env (EvBind { eb_lhs = var, eb_rhs = term, eb_is_given = is_given })
       ; return (EvBind { eb_lhs = var', eb_rhs = term', eb_is_given = is_given }) }
 
 zonkEvInstanceOf :: ZonkEnv -> EvInstanceOf -> TcM EvInstanceOf
-zonkEvInstanceOf _ EvInstanceOfRefl
-  = return EvInstanceOfRefl
-zonkEvInstanceOf env (EvInstanceOfEq co)
-  = do { co' <- zonkTcCoToCo env co
-       ; return (EvInstanceOfEq co') }
 zonkEvInstanceOf env (EvInstanceOfInst tys co q)
   = do { tys' <- mapM (zonkTcTypeToType env) tys
        ; let co' = zonkIdOcc env co
        ; q' <- mapM (zonkEvTerm env) q
        ; return (EvInstanceOfInst tys' co' q') }
+zonkEvInstanceOf env (EvInstanceOfInstEq tys co q)
+  = do { tys' <- mapM (zonkTcTypeToType env) tys
+       ; co' <- zonkTcCoToCo env co
+       ; q' <- mapM (zonkEvTerm env) q
+       ; return (EvInstanceOfInstEq tys' co' q') }
 zonkEvInstanceOf env (EvInstanceOfGen tys qvars bnds i)
   = do { (env', tys') <- zonkTyBndrsX env tys
        ; let qvars' = map (zonkIdOcc env') qvars
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index c5765a5457..f1aa3c580e 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -782,8 +782,7 @@ tcInstDecls2 tycl_decls inst_decls
         ; let dm_binds = unionManyBags dm_binds_s
 
           -- (b) instance declarations
-        ; let dm_ids = [(id, TcIdUnrestricted)
-                       | id <- collectHsBindsBinders dm_binds]
+        ; let dm_ids = collectHsBindsBinders dm_binds
               -- Add the default method Ids (again)
               -- See Note [Default methods and instances]
         ; inst_binds_s <- tcExtendLetEnv TopLevel dm_ids $
diff --git a/compiler/typecheck/TcMatches.hs b/compiler/typecheck/TcMatches.hs
index f6932c500f..56b6ff05bf 100644
--- a/compiler/typecheck/TcMatches.hs
+++ b/compiler/typecheck/TcMatches.hs
@@ -460,11 +460,10 @@ tcLcStmt m_tc ctxt (TransStmt { trS_form = form, trS_stmts = stmts
              -- See Note [GroupStmt binder map] in HsExpr
              n_bndr_ids  = zipWith mk_n_bndr n_bndr_names bndr_ids
              bindersMap' = bndr_ids `zip` n_bndr_ids
-             n_bndr_ids' = [(id, TcIdMonomorphic) | id <- n_bndr_ids]
 
        -- Type check the thing in the environment with
        -- these new binders and return the result
-       ; thing <- tcExtendIdEnv n_bndr_ids' (thing_inside elt_ty)
+       ; thing <- tcExtendIdEnv n_bndr_ids (thing_inside elt_ty)
 
        ; return (emptyTransStmt { trS_stmts = stmts', trS_bndrs = bindersMap'
                                 , trS_by = fmap fst by', trS_using = final_using
@@ -632,11 +631,10 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
              -- See Note [GroupStmt binder map] in HsExpr
              n_bndr_ids = zipWith mk_n_bndr n_bndr_names bndr_ids
              bindersMap' = bndr_ids `zip` n_bndr_ids
-             n_bndr_ids' = [(id, TcIdMonomorphic) | id <- n_bndr_ids]
 
        -- Type check the thing in the environment with
        -- these new binders and return the result
-       ; thing <- tcExtendIdEnv n_bndr_ids' (thing_inside new_res_ty)
+       ; thing <- tcExtendIdEnv n_bndr_ids (thing_inside new_res_ty)
 
        ; return (TransStmt { trS_stmts = stmts', trS_bndrs = bindersMap'
                            , trS_by = by', trS_using = final_using
@@ -786,9 +784,8 @@ tcDoStmt ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names
         ; tup_elt_tys <- newFlexiTyVarTys (length tup_names) liftedTypeKind
         ; let tup_ids  = zipWith mkLocalId tup_names tup_elt_tys
               tup_ty   = mkBigCoreTupTy tup_elt_tys
-              tup_ids' = [(tup_id, TcIdMonomorphic) | tup_id <- tup_ids]
 
-        ; tcExtendIdEnv tup_ids' $ do
+        ; tcExtendIdEnv tup_ids $ do
         { stmts_ty <- newFlexiTyVarTy liftedTypeKind
         ; (stmts', (ret_op', tup_rets))
                 <- tcStmtsAndThen ctxt tcDoStmt stmts stmts_ty   $ \ inner_res_ty ->
diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs
index 3c521cf27a..bec80ca5e2 100644
--- a/compiler/typecheck/TcPat.hs
+++ b/compiler/typecheck/TcPat.hs
@@ -497,7 +497,7 @@ tc_pat  :: PatEnv
 
 tc_pat penv (VarPat name) pat_ty thing_inside
   = do  { (co, id) <- tcPatBndr penv name pat_ty
-        ; res <- tcExtendIdEnv1 name id (chooseInstFlavor pat_ty) thing_inside
+        ; res <- tcExtendIdEnv1 name id thing_inside
         ; return (mkHsWrapPatCo co (VarPat id) pat_ty, res) }
 
 tc_pat penv (ParPat pat) pat_ty thing_inside
@@ -534,7 +534,7 @@ tc_pat _ (WildPat _) pat_ty thing_inside
 
 tc_pat penv (AsPat (L nm_loc name) pat) pat_ty thing_inside
   = do  { (co, bndr_id) <- setSrcSpan nm_loc (tcPatBndr penv name pat_ty)
-        ; (pat', res) <- tcExtendIdEnv1 name bndr_id (chooseInstFlavor pat_ty) $
+        ; (pat', res) <- tcExtendIdEnv1 name bndr_id $
                          tc_lpat pat (idType bndr_id) penv thing_inside
             -- NB: if we do inference on:
             --          \ (y@(x::forall a. a->a)) = e
@@ -671,7 +671,7 @@ tc_pat penv (NPlusKPat (L nm_loc name) (L loc lit) ge minus) pat_ty thing_inside
         ; icls <- tcLookupClass integralClassName
         ; instStupidTheta orig [mkClassPred icls [pat_ty']]
 
-        ; res <- tcExtendIdEnv1 name bndr_id (chooseInstFlavor pat_ty) thing_inside
+        ; res <- tcExtendIdEnv1 name bndr_id thing_inside
         ; return (mkHsWrapPatCo co pat' pat_ty, res) }
 
 tc_pat _ _other_pat _ _ = panic "tc_pat"        -- ConPatOut, SigPatOut
@@ -686,13 +686,6 @@ unifyPatType actual_ty expected_ty
   = do { coi <- unifyType actual_ty expected_ty
        ; return (mkTcSymCo coi) }
 
-chooseInstFlavor :: TcSigmaType -> TcIdFlavor
-chooseInstFlavor ty
-    -- if type is a variable, we need to add a monomorphic
-    -- flag for the environment
-  | Just _ <- tcGetTyVar_maybe ty = TcIdMonomorphic
-  | otherwise                     = TcIdUnrestricted
-
 {-
 Note [Hopping the LIE in lazy patterns]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index fd4ea4fd8e..adfa0a9f36 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -1451,8 +1451,7 @@ runTcInteractive hsc_env thing_inside
       | AnId id <- thing
       , NotTopLevel <- isClosedLetBndr id
       = Left (idName id, ATcId { tct_id = id
-                               , tct_closed = NotTopLevel
-                               , tct_flavor = TcIdUnrestricted })
+                               , tct_closed = NotTopLevel })
       | otherwise
       = Right thing
 
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 5ab11b03fb..d3a485aaeb 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -35,7 +35,7 @@ module TcRnTypes(
 
         -- Typechecker types
         TcTypeEnv, TcIdBinderStack, TcIdBinder(..),
-        TcTyThing(..), PromotionErr(..), TcIdFlavor(..),
+        TcTyThing(..), PromotionErr(..),
         SelfBootInfo(..),
         pprTcTyThingCategory, pprPECategory,
 
@@ -819,7 +819,6 @@ data TcTyThing
 
   | ATcId   {           -- Ids defined in this module; may not be fully zonked
         tct_id     :: TcId,
-        tct_flavor :: TcIdFlavor,
         tct_closed :: TopLevelFlag }   -- See Note [Bindings with closed types]
 
   | ATyVar  Name TcTyVar        -- The type variable to which the lexically scoped type
@@ -834,10 +833,6 @@ data TcTyThing
 
   | APromotionErr PromotionErr
 
-data TcIdFlavor
-  = TcIdMonomorphic
-  | TcIdUnrestricted
-
 data PromotionErr
   = TyConPE          -- TyCon used in a kind before we are ready
                      --     data T :: T -> * where ...
diff --git a/compiler/typecheck/TcRules.hs b/compiler/typecheck/TcRules.hs
index 1cd803ee78..f439675f3d 100644
--- a/compiler/typecheck/TcRules.hs
+++ b/compiler/typecheck/TcRules.hs
@@ -27,7 +27,6 @@ import Outputable
 import FastString
 import Bag
 import Data.List( partition )
-import Inst( newWanted )
 
 {-
 Note [Typechecking rules]
@@ -69,10 +68,9 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
               -- the RULE.  c.f. Trac #10072
 
        ; let (id_bndrs, tv_bndrs) = partition isId vars
-             id_bndrs' = [(id_bndr, choose_tc_id_flavor id_bndr) | id_bndr <- id_bndrs]
        ; (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty)
-            <- tcExtendTyVarEnv tv_bndrs  $
-               tcExtendIdEnv    id_bndrs' $
+            <- tcExtendTyVarEnv tv_bndrs $
+               tcExtendIdEnv    id_bndrs $
                do { -- See Note [Solve order for RULES]
                     ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
                   ; (rhs', rhs_wanted) <- captureConstraints (tcPolyMonoExpr rhs rule_ty)
@@ -138,11 +136,6 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
                     (mkHsDictLet (TcEvBinds lhs_binds_var) lhs') fv_lhs
                     (mkHsDictLet (TcEvBinds rhs_binds_var) rhs') fv_rhs) }
 
-choose_tc_id_flavor :: Id -> TcIdFlavor
-choose_tc_id_flavor v
-  | Just _ <- tcGetTyVar_maybe (idType v) = TcIdMonomorphic
-  | otherwise = TcIdUnrestricted
-
 tcRuleBndrs :: [LRuleBndr Name] -> TcM [Var]
 tcRuleBndrs []
   = return []
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index f29b36fa12..b27e4f693b 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -65,7 +65,7 @@ module TcType (
   -- Again, newtypes are opaque
   eqType, eqTypes, eqPred, cmpType, cmpTypes, cmpPred, eqTypeX,
   tcEqType, tcEqKind,
-  isSigmaTy, isRhoTy, isOverloadedTy,
+  isSigmaTy, isRhoTy, isOverloadedTy, isUpsilonTy,
   isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
   isIntegerTy, isBoolTy, isUnitTy, isCharTy,
   isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
@@ -1424,6 +1424,13 @@ isOverloadedTy (ForAllTy _ ty) = isOverloadedTy ty
 isOverloadedTy (FunTy a _)     = isPredTy a
 isOverloadedTy _               = False
 
+isUpsilonTy :: Type -> Bool
+isUpsilonTy ty
+  | isSigmaTy ty = False
+  | Just v       <- tcGetTyVar_maybe ty      = not (isImmutableTyVar v)
+  | Just (tc, _) <- tcSplitTyConApp_maybe ty = isFamilyTyCon tc
+  | otherwise    = True
+
 isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy,
     isUnitTy, isCharTy, isAnyTy :: Type -> Bool
 isFloatTy      = is_tc floatTyConKey
diff --git a/docs/types/impredicativity.ltx b/docs/types/impredicativity.ltx
index 8d3eecbb60..579dd4f851 100644
--- a/docs/types/impredicativity.ltx
+++ b/docs/types/impredicativity.ltx
@@ -39,7 +39,7 @@
 \begin{itemize}
 \item The kind of $\leq$ is $* \to * \to Constraint$.
 \item The evidence for $\sigma_1 \leq \sigma_2$ is a function $\sigma_1 \to \sigma_2$.
-\item The canonical forms are $\sigma \leq \alpha$, where $\alpha$ is not a Skolem.
+\item The canonical forms are $(\forall \overline{a}. Q \Rightarrow \sigma) \leq \upsilon$, where $\upsilon$ is either a unification variable or a type family application.
 \item In Haskell code, $\sigma_1 \leq \sigma_2$ is written as {\tt sigma1 <$\sim$ sigma2}.
 \end{itemize}
 
@@ -58,12 +58,16 @@ Type classes & $\mathtt{C}$
 Monomorphic types & $\mu$ & $\coloncolonequals$ & $\alpha \alt a \alt \mu_1 \to \mu_2 \alt \mathsf{T} \; \overline{\mu} \alt \mathsf{F} \; \overline{\mu}$ \\
 Types without top-level $\forall$ & $\tau$ & $\coloncolonequals$ & $\alpha \alt a \alt \sigma_1 \to \sigma_2 \alt \mathsf{T} \; \overline{\sigma} \alt \mathsf{F} \; \overline{\mu}$ \\
 Polymorphic types & $\sigma$ & $\coloncolonequals$ & $\forall \overline{a}. Q \Rightarrow \sigma \alt \tau$ \\
-Constraints & $Q$ & $\coloncolonequals$ & $\epsilon \alt Q_1 \wedge Q_2 \alt \sigma_1 \sim \sigma_2 \alt \sigma_1 \leq \sigma_2 \alt \mathtt{C} \; \overline{\mu}$ \\
+\\
+Instantiable types & $\psi$ & $\coloncolonequals$ & $a \alt \sigma_1 \to \sigma_2 \alt \mathsf{T} \; \overline{\sigma}$ \\
+Instantiable-or-polymorphic & $\psi^*$ & $\coloncolonequals$ & $\psi \alt \forall \overline{a}. Q \Rightarrow \sigma$ \\
+Non-instantiable types & $\upsilon$ & $\coloncolonequals$ & $\alpha \alt \mathsf{F} \; \overline{\mu}$ \\
+\\
+Constraints & $Q$ & $\coloncolonequals$ & $\epsilon \alt Q_1 \wedge Q_2 \alt \sigma_1 \sim \sigma_2 \alt \psi^*_1 \leq \sigma_2 \alt \mathtt{C} \; \overline{\mu}$ \\
 Implications & $I$ & $\coloncolonequals$ & $\epsilon \alt I_1 \wedge I_2 \alt Q \alt \forall \overline{a}. \, (Q \supset I)$ \\
-Canonical constraints & $Q^*$ & $\coloncolonequals$ & $\alpha \sim \sigma \alt \mathsf{F} \; \overline{\mu} \sim \sigma \alt \sigma \leq \alpha \alt \mathtt{C} \; \overline{\mu}$ \\
+Canonical constraints & $Q^*$ & $\coloncolonequals$ & $\upsilon \sim \sigma \alt a \sim \sigma \alt (\forall \overline{a}. Q \Rightarrow \sigma) \leq \upsilon \alt \mathtt{C} \; \overline{\mu}$ \\
 \\
-Family-free types & $\xi$ & $\coloncolonequals$ & $\alpha \alt a \alt \xi_1 \to \xi_2 \alt \mathsf{T} \; \overline{\xi}$ \\
-Instantiatiable types & $\psi$ & $\coloncolonequals$ & $a \alt \sigma_1 \to \sigma_2 \alt \mathsf{T} \; \overline{\sigma} \alt \mathsf{F} \; \overline{\mu}$
+Family-free types & $\xi$ & $\coloncolonequals$ & $\alpha \alt a \alt \xi_1 \to \xi_2 \alt \mathsf{T} \; \overline{\xi}$
 \end{tabular}
 \end{mdframed}
 \caption{Grammar}
@@ -95,13 +99,10 @@ $$
 \begin{figure}
 $$
 \begin{array}{lrcl}
-\textsc{[$\leq$refl]} & canon\left[\sigma \leq \sigma\right] & = & \epsilon \\
-\textsc{[$\leq$lcon]} & canon\left[\sigma_1 \leq \sigma_2\right] & = & \sigma_1 \sim \sigma_2 \\
-& & & \textrm{where } \sigma_1 \not\equiv \sigma_2, \sigma_1 \not\equiv \forall \overline{a}. Q \Rightarrow \sigma'_1 \\
-% \textsc{[$\leq$l$\forall$var]} & canon\left[(\forall \overline{a}. Q_1 \Rightarrow v) \leq \psi_2 \right] & = & [\overline{a \mapsto \alpha}]v \sim \psi_2 \, \wedge \, [\overline{a \mapsto \alpha}]Q_1 \\
-% & & & \textrm{where } v \textrm{ is a unification variable and } v \in \overline{a} \\
-\textsc{[$\leq$l$\forall$]} & canon\left[(\forall \overline{a}. Q_1 \Rightarrow \sigma_1) \leq \psi_2\right] & = & [\overline{a \mapsto \alpha}]\sigma_1 \leq \sigma_2 \, \wedge \, [\overline{a \mapsto \alpha}]Q_1 \\
-% & & & \textrm{where } v \textrm{ is not a unification variable or } v \not\in \overline{a} \\
+\textsc{[$\leq$l$\tau$r$\tau$]} & canon\left[\tau_1 \leq \tau_2\right] & = & \tau_1 \sim \tau_2 \\
+\textsc{[$\leq$l$\forall\psi$r$\psi$]} & canon\left[(\forall \overline{a}. Q_1 \Rightarrow \psi^*_1) \leq \psi_2\right] & = & [\overline{a \mapsto \alpha}]\psi^*_1 \leq \psi_2 \, \wedge \, [\overline{a \mapsto \alpha}]Q_1 \\
+\textsc{[$\leq$l$\forall\upsilon$r$\psi$]} & canon\left[(\forall \overline{a}. Q_1 \Rightarrow \upsilon_1) \leq \psi_2\right] & = & [\overline{a \mapsto \alpha}]\upsilon_1 \sim \psi_2 \, \wedge \, [\overline{a \mapsto \alpha}]Q_1 \\
+\textsc{[$\leq$l$\forall\upsilon$r$\upsilon$]} & canon\left[(\forall \overline{a}. \upsilon_1) \leq \upsilon_2\right] & = & [\overline{a \mapsto \alpha}]\upsilon_1 \sim \upsilon_2 \\
 \textsc{[$\leq$r$\forall$]} & canon\left[\sigma_1 \leq (\forall \overline{a}. Q_2 \Rightarrow \sigma_2)\right] & = & \forall \overline{a}. \, (Q_2 \supset \sigma_1 \leq \sigma_2) \\
 \end{array}
 $$
@@ -125,7 +126,7 @@ the only constraint being generated is $(\forall\, a.\, \textit{Monoid} \; a \Ri
 
 \item We also disallow applying the rules to quantified types. In that case, we want to apply {\sc [$\leq$r$\forall$]} first, which may in turn lead to an application of the other rules inside the implication.
 
-\item Previously, these rules along with generation and propagation worked very hard to ensure that no constraint of the form $\alpha \leq \sigma$, with $\alpha$ a unification variable, was ever produced.
+\item Previously, these rules along with generation and propagation worked very hard to ensure that no constraint $\alpha \leq \sigma$, with $\alpha$ a unification variable, was ever produced.
 
 Nonetheless, there was still the chance that $\alpha \leq \sigma$ is produced from a constraint involving a type family $\mathsf{F} \; \alpha \leq \sigma$ whose family resolves to a variable $\mathsf{F} \; \alpha \sim \alpha$. Since we do not want to loose confluence, we ensure that this resolves to $\alpha \sim \sigma$ regardless of the order of application of rule {\sc [$\leq$lcon]} and type family rewriting.
 
@@ -272,13 +273,6 @@ We prefer this option for the approximation phase in inference, since it leads t
 
 In the $\Gamma \vdash e : \sigma \leadsto C$ judgement, $\Gamma$ and $e$ are inputs, whereas $\sigma$ and $C$ are outputs. The highlighted parts are changes with respect to the constraint generation judgement in the original {\sc OutsideIn(X)} system.
 
-\highlighttree{
-\begin{prooftree}
-\AxiomC{$x :_\lambda \tau \in \Gamma$}
-\RightLabel{\sc VarCon${}_\lambda$}
-\UnaryInfC{$\Gamma \vdash x : \tau \leadsto \epsilon$}
-\end{prooftree}}
-
 \begin{prooftree}
 \AxiomC{$\alpha$ fresh}
 \AxiomC{$x : \sigma \in \Gamma$}
@@ -288,7 +282,7 @@ In the $\Gamma \vdash e : \sigma \leadsto C$ judgement, $\Gamma$ and $e$ are inp
 
 \begin{prooftree}
 \AxiomC{$\alpha$ fresh}
-\AxiomC{$\Gamma, \highlight{x :_\lambda \alpha} \vdash e : \tau \leadsto C$}
+\AxiomC{$\Gamma, x : \alpha \vdash e : \tau \leadsto C$}
 \RightLabel{\sc Abs}
 \BinaryInfC{$\Gamma \vdash \lambda x. e : \alpha \to \tau \leadsto C$}
 \end{prooftree}
@@ -317,7 +311,7 @@ In the $\Gamma \vdash e : \sigma \leadsto C$ judgement, $\Gamma$ and $e$ are inp
 
 \begin{prooftree}
 \AxiomC{$\Gamma \vdash e_1 : \tau_1 \leadsto C_1$}
-\AxiomC{$\Gamma, \highlight{x :_\lambda \tau_1} \vdash e_2 : \tau_2 \leadsto C_2$}
+\AxiomC{$\Gamma, x : \tau_1 \vdash e_2 : \tau_2 \leadsto C_2$}
 \RightLabel{\sc Let}
 \BinaryInfC{$\Gamma \vdash \textsf{let } x = e_1 \textsf{ in } e_2 : \tau_2 \leadsto C_1 \wedge C_2$}
 \end{prooftree}
@@ -349,34 +343,6 @@ $}
 \UnaryInfC{$\Gamma \vdash \textsf{case } e \textsf{ of } \{ \overline{K_i \, \overline{x_i} \to u_i} \} : \beta \leadsto C \wedge \textsf{T} \, \overline{\gamma} \sim \tau \wedge \bigwedge C'_i$}
 \end{prooftree}
 
-\subsection*{Why $:_\lambda$?}
-
-In principle, the only rule that wuld need to change is that of variables in the term level, which is the point in which instantiation may happen:
-\begin{prooftree}
-\AxiomC{$\alpha$ fresh}
-\AxiomC{$x : \sigma \in \Gamma$}
-\RightLabel{\sc VarCon}
-\BinaryInfC{$\Gamma \vdash x : \alpha \leadsto \highlight{\sigma \leq \alpha}$}
-\end{prooftree}
-Unfortunately, this is not enough. Suppose we have the following piece of code:
-\begin{verbatim}
-(\f -> (f 1, f True)) (if ... then id else not)
-\end{verbatim}
-We want to typecheck it, and we give the argument $f$ a type variable $\alpha$, and each of its appearances the types variables $\beta$ and $\gamma$. The constraints that are generated are:
-\begin{itemize}
-\item $\alpha \leq \beta$ (from the usage in {\tt f 1})
-\item $\alpha \leq \gamma$ (from the usage in {\tt f True})
-\item $(\forall a. \, a \to a) \leq \alpha$ (from {\tt id})
-\item $(Bool \to Bool) \leq \alpha$ (from {\tt not})
-\end{itemize}
-At this point we are stuck, since we have no rule that could be applied. One might think about applying some kind transitivity of $\leq$, but this is just calling trouble, because it is not clear how to do this without losing information.
-
-\
-
-Our solution is to make this situation impossible by generating $\alpha \sim \beta$ and $\alpha \sim \gamma$ instead of their $\leq$ counterparts. We do this by splitting the {\sc [VarCon]} rule in such a way that $\sim$ is generated when the variable comes from an unannotated abstraction or unannotated $\mathsf{let}$. The environment is responsible for keeping track of this fact for each binding, by a small tag, which we denote by $:_\lambda$ in the type rules.
-
-With this change, our initial example leads to an error ({\tt f cannot be applied to both Bool and Int}), from which one can recover by adding an extra annotation. This is a better situation, though, that getting stuck in the middle of the solving process.
-
 \subsection*{With propagation}
 
 \noindent We use propagation to cover two main scenarios:
@@ -394,12 +360,6 @@ f = \x. -> (x 1, x True)
 \noindent In the $\Gamma \vdash_\Downarrow e : \sigma \leadsto C$ judgement, $\Gamma$, $e$ and $\sigma$ are inputs, and only $C$ is an output.
 
 \begin{prooftree}
-\AxiomC{$x :_\lambda \tau \in \Gamma$}
-\RightLabel{\sc VarCon${}_\lambda$}
-\UnaryInfC{$\Gamma \vdash_\Downarrow x : \sigma \leadsto \tau \sim \sigma$}
-\end{prooftree}
-
-\begin{prooftree}
 \AxiomC{$x : \sigma_1 \in \Gamma$}
 \RightLabel{\sc VarCon}
 \UnaryInfC{$\Gamma \vdash_\Downarrow x : \sigma_2 \leadsto \sigma_1 \leq \sigma_2$}
@@ -413,29 +373,15 @@ f = \x. -> (x 1, x True)
 
 \begin{prooftree}
 \AxiomC{$\alpha$, $\beta$ fresh}
-\AxiomC{$\Gamma, x :_\lambda \alpha \vdash_\Downarrow e : \beta \leadsto C$}
+\AxiomC{$\Gamma, x : \alpha \vdash_\Downarrow e : \beta \leadsto C$}
 \RightLabel{\sc AbsVar}
 \BinaryInfC{$\Gamma \vdash_\Downarrow \lambda x. e : \gamma \leadsto C \, \wedge \, \gamma \sim \alpha \to \beta$}
 \end{prooftree}
 
 \begin{prooftree}
-\AxiomC{$\Gamma, x :_\lambda \alpha \vdash_\Downarrow e : \sigma_2 \leadsto C$}
-\RightLabel{\sc AbsArrowVar}
-\UnaryInfC{$\Gamma \vdash_\Downarrow \lambda x. e : \alpha \to \sigma_2 \leadsto C$}
-\end{prooftree}
-
-\begin{prooftree}
-\AxiomC{$\Gamma, x : \forall a. \sigma_1 \vdash_\Downarrow e : \sigma_2 \leadsto C$}
-\RightLabel{\sc AbsArrow$\forall$}
-\UnaryInfC{$\Gamma \vdash_\Downarrow \lambda x. e : (\forall a. \sigma_1) \to \sigma_2 \leadsto C$}
-\end{prooftree}
-
-\begin{prooftree}
-\AxiomC{$\sigma_1 \not\equiv \alpha$}
-\AxiomC{$\sigma_1 \not\equiv \forall a. Q \Rightarrow \sigma$}
-\AxiomC{$\Gamma, x :_{\{\lambda,\_\}} \sigma_1 \vdash_\Downarrow e : \sigma_2 \leadsto C$}
-\RightLabel{\sc AbsArrowRest}
-\TrinaryInfC{$\Gamma \vdash_\Downarrow \lambda x. e : \sigma_1 \to \sigma_2 \leadsto C$}
+\AxiomC{$\Gamma, x : \sigma_1 \vdash_\Downarrow e : \sigma_2 \leadsto C$}
+\RightLabel{\sc AbsArrow}
+\UnaryInfC{$\Gamma \vdash_\Downarrow \lambda x. e : \sigma_1 \to \sigma_2 \leadsto C$}
 \end{prooftree}
 
 \begin{prooftree}
@@ -457,28 +403,15 @@ f = \x. -> (x 1, x True)
 \noLine
 \BinaryInfC{
 $\theta = [\overline{a \to \alpha}] \qquad
-\Gamma \vdash_\Downarrow e_i : \theta(\sigma_i) \leadsto C_i \qquad
-\theta(\sigma_r) \equiv \beta$}
-\RightLabel{\sc AppFunVar}
-\UnaryInfC{$\Gamma \vdash_\Downarrow f \, e_1 \, \dots \, e_n : \sigma \leadsto \bigwedge_i C_i \, \wedge \, \theta(Q) \, \wedge \, \theta(\sigma_r) \sim \sigma$}
-\end{prooftree}
-
-\begin{prooftree}
-\AxiomC{$f \in \Gamma$}
-\AxiomC{$f : \forall \overline{a}. \, \sigma_1 \to \dots \to \sigma_n \to \sigma_r \in \Gamma$}
-\noLine
-\BinaryInfC{
-$\theta = [\overline{a \to \alpha}] \qquad
-\Gamma \vdash_\Downarrow e_i : \theta(\sigma_i) \leadsto C_i \qquad
-\theta(\sigma_r) \not\equiv \beta$}
-\RightLabel{\sc AppFunNonVar}
+\Gamma \vdash_\Downarrow e_i : \theta(\sigma_i) \leadsto C_i$}
+\RightLabel{\sc AppFun}
 \UnaryInfC{$\Gamma \vdash_\Downarrow f \, e_1 \, \dots \, e_n : \sigma \leadsto \bigwedge_i C_i \, \wedge \, \theta(Q) \, \wedge \, \theta(\sigma_r) \leq \sigma$}
 \end{prooftree}
 
 \begin{prooftree}
+\AxiomC{$\alpha \text{ fresh}$}
 \AxiomC{$\Gamma \vdash_\Downarrow e_1 : \alpha \to \sigma \leadsto C_1$}
 \AxiomC{$\Gamma \vdash_\Downarrow e_2 : \alpha \leadsto C_2$}
-\AxiomC{$\alpha \text{ fresh}$}
 \RightLabel{\sc App}
 \TrinaryInfC{$\Gamma \vdash_\Downarrow e_1 \, e_2 : \sigma \leadsto C_1 \, \wedge \, C_2$}
 \end{prooftree}
@@ -491,8 +424,8 @@ $\theta = [\overline{a \to \alpha}] \qquad
 
 \begin{prooftree}
 \AxiomC{$\alpha$ fresh}
-\AxiomC{$\Gamma, x :_\lambda \alpha \vdash_\Downarrow e_1 : \alpha \leadsto C_1$}
-\AxiomC{$\Gamma, x :_\lambda \alpha \vdash_\Downarrow e_2 : \sigma \leadsto C_2$}
+\AxiomC{$\Gamma, x : \alpha \vdash_\Downarrow e_1 : \alpha \leadsto C_1$}
+\AxiomC{$\Gamma, x : \alpha \vdash_\Downarrow e_2 : \sigma \leadsto C_2$}
 \RightLabel{\sc Let}
 \TrinaryInfC{$\Gamma \vdash_\Downarrow \textsf{let } x = e_1 \textsf{ in } e_2 : \sigma \leadsto C_1 \, \wedge \, C_2$}
 \end{prooftree}
@@ -527,19 +460,128 @@ $}
 
 \
 
-\noindent The most surprising rules are {\sc [AppFunVar]} and {\sc [AppFunNonVar]}, which apply when we have a known expression $f$ whose type can be recovered from the environment followed by some other freely-shaped expressions. For example, the case of {\tt f (\\x -> x)} above, where {\tt f} is in the environment. In that case, we compute the type that the first block ought to have, and propagate it to the rest of arguments.
+\noindent The most surprising rule is {\sc [AppFun]}, which applies when we have a known expression $f$ whose type can be recovered from the environment followed by some other freely-shaped expressions. For example, the case of {\tt f ($\backslash$x -> x)} above, where {\tt f} is in the environment. In that case, we compute the type that the first block ought to have, and propagate it to the rest of arguments.
 
 % The reason for including a block of $f_i$s is to cover cases such as {\tt runST $ do ...}, or more clearly {\tt ($) runST (do ...)}, where some combinators are used between functions. Should the rules only include the case $f \, e_1 \, \dots \, f_m$, the fairly common {\tt runST $ do ...} could not be typed without an annotation.
 
-Of course, there is a reason for distinguishing between the cases of the return type being a variable or not, and generating equalities or instantiation constraints. In short, there is a reason for having both {\sc [AppFunVar]} and {\sc [AppFunNonVar]}. Consider the following:
+\subsection*{Why (not) $:_\lambda$?}
+
+In this section, we describe the thought process that led to the rule {\sc [$\leq$lcon]} to be applied to unification variables in the left-hand side, and not only to types headed by a constructor, as we first thought.
+
+\
+
+In principle, the only rule that would need to change is that of variables in the term level, which is the point in which instantiation may happen:
+\begin{prooftree}
+\AxiomC{$\alpha$ fresh}
+\AxiomC{$x : \sigma \in \Gamma$}
+\RightLabel{\sc VarCon}
+\BinaryInfC{$\Gamma \vdash x : \alpha \leadsto \highlight{\sigma \leq \alpha}$}
+\end{prooftree}
+Unfortunately, if {\sc [$\leq$lcon]} cannot be applied to unification variables in the left-hand side, this is not enough. Suppose we have the following piece of code:
+\begin{verbatim}
+(\f -> (f 1, f True)) (if ... then id else not)
+\end{verbatim}
+We want to typecheck it, and we give the argument $f$ a type variable $\alpha$, and each of its appearances the types variables $\beta$ and $\gamma$. The constraints that are generated are:
+\begin{itemize}
+\item $\alpha \leq \beta$ (from the usage in {\tt f 1})
+\item $\alpha \leq \gamma$ (from the usage in {\tt f True})
+\item $(\forall a. \, a \to a) \leq \alpha$ (from {\tt id})
+\item $(Bool \to Bool) \leq \alpha$ (from {\tt not})
+\end{itemize}
+At this point we are stuck, since we have no rule that could be applied. One might think about applying some kind transitivity of $\leq$, but this is just calling trouble, because it is not clear how to do this without losing information.
+
+\
+
+The first solution is to make this situation impossible by generating $\alpha \sim \beta$ and $\alpha \sim \gamma$ instead of their $\leq$ counterparts. We do this by splitting the {\sc [VarCon]} rule in such a way that $\sim$ is generated when the variable comes from an unannotated abstraction or unannotated $\mathsf{let}$. The environment is responsible for keeping track of this fact for each binding, by a small tag, which we denote by $:_\lambda$ in the type rules.
+\begin{prooftree}
+\AxiomC{$\highlight{x :_\lambda \tau} \in \Gamma$}
+\RightLabel{\sc VarCon${}_\lambda$}
+\UnaryInfC{$\Gamma \vdash x : \tau \leadsto \epsilon$}
+\end{prooftree}
+\begin{prooftree}
+\AxiomC{$\alpha$ fresh}
+\AxiomC{$\Gamma, \highlight{x :_\lambda \alpha} \vdash e : \tau \leadsto C$}
+\RightLabel{\sc Abs}
+\BinaryInfC{$\Gamma \vdash \lambda x. e : \alpha \to \tau \leadsto C$}
+\end{prooftree}
+\begin{prooftree}
+\AxiomC{$\Gamma \vdash e_1 : \tau_1 \leadsto C_1$}
+\AxiomC{$\Gamma, \highlight{x :_\lambda \tau_1} \vdash e_2 : \tau_2 \leadsto C_2$}
+\RightLabel{\sc Let}
+\BinaryInfC{$\Gamma \vdash \textsf{let } x = e_1 \textsf{ in } e_2 : \tau_2 \leadsto C_1 \wedge C_2$}
+\end{prooftree}
+With this change, our initial example leads to an error ({\tt f cannot be applied to both Bool and Int}), from which one can recover by adding an extra annotation. This is a better situation, though, that getting stuck in the middle of the solving process.
+
+\
+
+This was not the only change that was needed to ensure that $\alpha \leq \sigma$ is not produced. You need also a special case of the rule {\sc [$\leq$l$\forall$]} when the body of a $\sigma$-type is a single variable:
+$$
+\begin{array}{lrcl}
+\textsc{[$\leq$l$\forall$var]} & canon\left[(\forall \overline{a}. Q_1 \Rightarrow v) \leq \psi_2 \right] & = & [\overline{a \mapsto \alpha}]v \sim \psi_2 \, \wedge \, [\overline{a \mapsto \alpha}]Q_1 \\
+& & & \textrm{where } v \textrm{ is a unification variable and } v \in \overline{a}
+\end{array}
+$$
+And a special case for the {\sc AppFun} rule of propagation:
+\begin{prooftree}
+\AxiomC{$f \in \Gamma$}
+\AxiomC{$f : \forall \overline{a}. \, \sigma_1 \to \dots \to \sigma_n \to \sigma_r \in \Gamma$}
+\noLine
+\BinaryInfC{
+$\theta = [\overline{a \to \alpha}] \qquad
+\Gamma \vdash_\Downarrow e_i : \theta(\sigma_i) \leadsto C_i \qquad
+\theta(\sigma_r) \equiv \beta$}
+\RightLabel{\sc AppFunVar}
+\UnaryInfC{$\Gamma \vdash_\Downarrow f \, e_1 \, \dots \, e_n : \sigma \leadsto \bigwedge_i C_i \, \wedge \, \theta(Q) \, \wedge \, \theta(\sigma_r) \sim \sigma$}
+\end{prooftree}
+For the case of the special {\sc AppFun} rule, consider the following:
 \begin{verbatim}
 data S a = S a
 
 f :: [Char] -> S a
 f x = S (error x)
 \end{verbatim}
-If we apply {\sc [AppFunNonVar]} directly, we instantiate the type of $error :: \forall b. [Char] \to b$ to $[Char] \to \beta$.
-Since we are pushing down a unification variable $\alpha$ because of the previous application of {\sc [AppFunNonVar]} to $S :: \forall a. \, a \to S \; a$, we obtain a constraint $\beta \leq \alpha$. Since there are no more restrictions to either $\alpha$ or $\beta$, we are not stuck in solving.
+If we apply {\sc [AppFun]} directly, we instantiate the type of $error :: \forall b. [Char] \to b$ to $[Char] \to \beta$. Since we are pushing down a unification variable $\alpha$ because of the previous application of {\sc [AppFun]} to $S :: \forall a. \, a \to S \; a$, we obtain a constraint $\beta \leq \alpha$. Since there are no more restrictions to either $\alpha$ or $\beta$, we are not stuck in solving.
+
+\
+
+Nevertheless, you could always end up in the situation described in the notes of the {\sc [$\leq$lcon]} rule, where a type family rewrites to a type variable. It is easier to just make $\alpha \leq \sigma$ rewrite to $\alpha \sim \sigma$ in any case (but when $\sigma$ is headed by $\forall$).
+This solution goes along with the following philosophy of impredicativity in our system:
+\begin{itemize}
+\item The system is impredicative in the sense that a polymorphic function may be instantiated at a polytype. Or more operationally, a unification variable may be unified with a polytype.
+\item But it does not follow that after being filled in with a polytype, a unification variable can then be instantiated.
+\end{itemize}
+
+\subsection*{{\tt f \$ x} is equivalent to {\tt f x}}
+
+One nice property of the system is that the rule {\sc AppFun} applied to the case {\tt f \$ x} for {\tt f} not in the environment is equivalent to the rule {\sc App} applied to {\tt f x}. In the first case we have:
+\begin{prooftree}
+\AxiomC{$\alpha, \beta$ fresh}
+\AxiomC{$\Gamma \vdash_\Downarrow f : \alpha \to \beta \leadsto C_1$}
+\AxiomC{$\Gamma \vdash_\Downarrow x : \alpha \leadsto C_2$}
+\TrinaryInfC{$\Gamma \vdash_\Downarrow f \; \$ \; x : \sigma \leadsto C_1 \wedge C_2 \wedge \beta \leq \sigma$}
+\end{prooftree}
+Note that we know that $\beta \leq \sigma$ will be readily changed to $\beta \sim \sigma$. And by substitution of equals, we get the rule:
+\begin{prooftree}
+\AxiomC{$\alpha$ fresh}
+\AxiomC{$\Gamma \vdash_\Downarrow f : \alpha \to \sigma \leadsto C_1$}
+\AxiomC{$\Gamma \vdash_\Downarrow x : \alpha \leadsto C_2$}
+\TrinaryInfC{$\Gamma \vdash_\Downarrow f \; \$ \; x : \sigma \leadsto C_1 \wedge C_2$}
+\end{prooftree}
+Which is exactly the {\sc App} rule applied to $f \; x$!
+
+\
+
+\noindent Note that this equivalence only holds in the case where {\sc App} would be applied to the expression {\tt f  x}. In particular, if $f \in \Gamma$, the rule {\sc AppFun} is chosen instead. If equivalence between {\tt f \$ x} and {\tt f x} is desired in this case, an extra rule needs to be added:
+\begin{prooftree}
+\AxiomC{$f \in \Gamma$}
+\AxiomC{$f : \forall \overline{a}. \, \sigma_s \to \sigma_r \in \Gamma$}
+\noLine
+\BinaryInfC{
+$\theta = [\overline{a \to \alpha}] \qquad
+\Gamma \vdash_\Downarrow e : \theta(\sigma_s) \leadsto C$}
+\RightLabel{\sc App\$Fun}
+\UnaryInfC{$\Gamma \vdash_\Downarrow f \, \$ \, e : \sigma \leadsto C \, \wedge \, \theta(Q) \, \wedge \, \theta(\sigma_r) \leq \sigma$}
+\end{prooftree}
 
 %\newpage
 \section*{Examples}