diff --git a/README.md b/README.md
index c741e85..4aa51c5 100644
--- a/README.md
+++ b/README.md
@@ -84,7 +84,6 @@ Information about external dependencies are presented in [INSTALL.md](INSTALL.md
 Things still missing
 ====================
 
-+ 'using' blocks
 + Disambiguation via 'with'
 + Cumulativity (so we currently have Type : Type! Bear that in mind when you
   think you've proved something :))
diff --git a/src/TTImp/Elab/Binders.idr b/src/TTImp/Elab/Binders.idr
index 400f0d0..058905a 100644
--- a/src/TTImp/Elab/Binders.idr
+++ b/src/TTImp/Elab/Binders.idr
@@ -174,7 +174,8 @@ checkLet rigc_in elabinfo nest env fc rigl n nTy nVal scope expty
          -- try checking at Rig1 (meaning that we're using a linear variable
          -- so the resulting binding should be linear)
          (valv, valt, rigb) <- handle
-              (do c <- check (rigMult rigl rigc) elabinfo
+              (do c <- check (rigMult rigl rigc)
+                             (record { preciseInf = True } elabinfo)
                              nest env nVal (Just (gnf env tyv))
                   pure (fst c, snd c, rigMult rigl rigc))
               (\err => case err of
diff --git a/src/TTImp/Elab/Check.idr b/src/TTImp/Elab/Check.idr
index dfbf004..efe223d 100644
--- a/src/TTImp/Elab/Check.idr
+++ b/src/TTImp/Elab/Check.idr
@@ -349,10 +349,12 @@ record ElabInfo where
   implicitMode : BindMode
   topLevel : Bool
   bindingVars : Bool
+  preciseInf : Bool -- are types inferred precisely (True) or do we generalise
+                    -- pi bindings to RigW (False, default)
 
 export
 initElabInfo : ElabMode -> ElabInfo
-initElabInfo m = MkElabInfo m NONE False True
+initElabInfo m = MkElabInfo m NONE False True False
 
 export
 tryError : {vars : _} ->
@@ -631,4 +633,4 @@ checkExp : {vars : _} ->
            (term : Term vars) ->
            (got : Glued vars) -> (expected : Maybe (Glued vars)) ->
            Core (Term vars, Glued vars)
-checkExp rig = checkExpP rig False
+checkExp rig elabinfo = checkExpP rig (preciseInf elabinfo) elabinfo