tcSkolemiseTypewip/rae-aug06

This function compiles, but is otherwise untested.

This commit also removes the unused checkTvConstraints.

4 files changed, 46 insertions, 20 deletions

diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index 85175b227a..facb8e5e52 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -432,11 +432,10 @@ instance Data.Data TcEvBinds where
 Class constraints etc give rise to /term/ bindings for evidence, and
 we have nowhere to put term bindings in /types/.  So in some places we
 use CoEvBindsVar (see newCoTcEvBinds) to signal that no term-level
-evidence bindings are allowed.  Notebly ():
+evidence bindings are allowed.  Notably:
 
   - Places in types where we are solving kind constraints (all of which
-    are equalities); see solveEqualities, solveLocalEqualities,
-    checkTvConstraints
+    are equalities); see solveEqualities and solveLocalEqualities
 
   - When unifying forall-types
 -}
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 4504f8c276..801b13c355 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1907,6 +1907,47 @@ kcLHsQTyVars_NonCusk name flav
 
 kcLHsQTyVars_NonCusk _ _ (XLHsQTyVars nec) _ = noExtCon nec
 
+-- Take a type and skolemise any quantified variables at the front.
+-- Does *not* deeply skolemise or bring anything into scope.
+-- The fresh skolems are substed into the type passed to the continuation
+-- Emits an implication constraint with a correct SkolemInfo, wrapping
+-- any constrainted emitted by the continuation.
+-- Is a no-op for types without any outermost quantification.
+-- Very much like TcUnify.tcSkolemise, but for types instead of terms.
+tcSkolemiseType :: UserTypeCtxt -> TcSigmaType
+                -> (TcType -> TcM r)
+                -> TcM r
+tcSkolemiseType ctxt expected_ty thing_inside
+  | null tvs
+  = thing_inside expected_ty
+
+  | otherwise
+  = do {
+         -- using tcInstSkolTyVars means that we have to inefficiently apply
+         -- the subst to the rest of the type instead of building up a
+         -- TCvSubst. This is quadratic in the number of user- written
+         -- foralls. I (Richard E) think this is an acceptable cost for code
+         -- simplicity.
+         (subst, skols) <- tcInstSkolTyVars tvs
+
+       ; traceTc "tcSkolemiseType" (vcat [ text "expected_ty:" <+> ppr expected_ty
+                                         , text "skols:" <+> ppr skols ])
+
+       ; let tv_prs = [ (getName tv, skol)
+                      | (tv, skol) <- zipEqual "tcSkolemiseType" tvs skols ]
+             skol_info = SigSkol ctxt expected_ty tv_prs
+
+             inner_ty' = substTy subst inner_ty
+
+       ; (tclvl, wanted, result)
+           <- pushLevelAndCaptureConstraints (thing_inside inner_ty')
+       ; emitResidualTvConstraint skol_info Nothing skols tclvl wanted
+
+       ; return result }
+  where
+    -- really, we want all *invisible* arguments, but
+    -- that's covered by tcSplitForAllTys for now
+    (tvs, inner_ty) = tcSplitForAllTys expected_ty
 
 {- Note [No polymorphic recursion]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 68496dfca6..8ecd377563 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -2854,8 +2854,7 @@ checkTvConstraintsTcS :: SkolemInfo
                       -> [TcTyVar]        -- Skolems
                       -> TcS (result, Cts)
                       -> TcS result
--- Just like TcUnify.checkTvConstraints, but
---   - In the TcS monnad
+-- Wraps the continuation in an implication binding the given skolems
 --   - The thing-inside should not put things in the work-list
 --     Instead, it returns the Wanted constraints it needs
 --   - No 'givens', and no TcEvBinds; this is type-level constraints only
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index 45cc3f9168..4776304688 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -14,7 +14,7 @@ module TcUnify (
   tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET,
   tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS,
   tcSubTypeDS_NC_O, tcSubTypeET,
-  checkConstraints, checkTvConstraints,
+  checkConstraints,
   buildImplicationFor, emitResidualTvConstraint,
 
   -- Various unifications
@@ -1084,6 +1084,7 @@ the thinking.
 -- | Take an "expected type" and strip off quantifiers to expose the
 -- type underneath, binding the new skolems for the @thing_inside@.
 -- The returned 'HsWrapper' has type @specific_ty -> expected_ty@.
+-- If you are processing a type instead of a term, see TcHsType.tcSkolemiseType
 tcSkolemise :: UserTypeCtxt -> TcSigmaType
             -> ([TcTyVar] -> TcType -> TcM result)
          -- ^ These are only ever used for scoped type variables.
@@ -1159,20 +1160,6 @@ checkConstraints skol_info skol_tvs given thing_inside
               do { res <- thing_inside
                  ; return (emptyTcEvBinds, res) } }
 
-checkTvConstraints :: SkolemInfo
-                   -> Maybe SDoc  -- User-written telescope, if present
-                   -> TcM ([TcTyVar], result)
-                   -> TcM ([TcTyVar], result)
-
-checkTvConstraints skol_info m_telescope thing_inside
-  = do { (tclvl, wanted, (skol_tvs, result))
-             <- pushLevelAndCaptureConstraints thing_inside
-
-       ; emitResidualTvConstraint skol_info m_telescope
-                                  skol_tvs tclvl wanted
-
-       ; return (skol_tvs, result) }
-
 emitResidualTvConstraint :: SkolemInfo -> Maybe SDoc -> [TcTyVar]
                          -> TcLevel -> WantedConstraints -> TcM ()
 emitResidualTvConstraint skol_info m_telescope skol_tvs tclvl wanted