1 files changed, 20 insertions, 14 deletions
diff --git a/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs b/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs
index 5bccfff..3eb54b1 100644
--- a/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs
+++ b/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs
@@ -1,8 +1,9 @@
 {-# LANGUAGE CPP           #-}
-{-# LANGUAGE TupleSections #-}
 
 module Agda.TypeChecking.Rules.LHS.ProblemRest where
 
+import Data.Functor ((<$))
+
 import Agda.Syntax.Common
 import Agda.Syntax.Internal
 import qualified Agda.Syntax.Abstract as A
@@ -11,7 +12,6 @@ import Agda.TypeChecking.Monad
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Telescope
 import Agda.TypeChecking.Substitute
-import Agda.TypeChecking.Substitute.Pattern
 
 import Agda.TypeChecking.Rules.LHS.Problem
 import Agda.TypeChecking.Rules.LHS.Implicit
@@ -26,18 +26,24 @@ import Agda.Utils.Impossible
 -- MOVED from LHS:
 -- | Rename the variables in a telescope using the names from a given pattern
 useNamesFromPattern :: [NamedArg A.Pattern] -> Telescope -> Telescope
-useNamesFromPattern ps = telFromList . zipWith ren (toPats ps ++ repeat dummy) . telToList
+useNamesFromPattern ps = telFromList . zipWith ren (map namedArg ps ++ repeat dummy) . telToList
   where
     dummy = A.WildP __IMPOSSIBLE__
-    ren (A.VarP x) (Dom info (_, a)) | notHidden info = Dom info (nameToArgName x, a)
+    ren (A.VarP x) (Dom info (_, a)) | notHidden info && not (isNoName x) =
+      Dom info (nameToArgName x, a)
     ren A.AbsurdP{} (Dom info (_, a)) | notHidden info = Dom info ("()", a)
     -- Andreas, 2013-03-13: inserted the following line in the hope to fix issue 819
     -- but it does not do the job, instead, it puts a lot of "_"s
     -- instead of more sensible names into error messages.
     -- ren A.WildP{}  (Dom info (_, a)) | notHidden info = Dom info ("_", a)
     ren A.PatternSynP{} _ = __IMPOSSIBLE__  -- ensure there are no syns left
+    -- Andreas, 2016-05-10, issue 1848: if context variable has no name, call it "x"
+    ren _ (Dom info (x, a)) | notHidden info && isNoName x =
+      Dom info (stringToArgName "x", a)
     ren _ a = a
-    toPats = map namedArg
+
+useOriginFrom :: (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a]
+useOriginFrom = zipWith $ \x y -> setOrigin (getOrigin y) x
 
 -- | Are there any untyped user patterns left?
 noProblemRest :: Problem -> Bool
@@ -74,7 +80,9 @@ problemFromPats ps a = do
   -- For the initial problem, do not insert trailing implicits.
   -- This has the effect of not including trailing hidden domains in the problem telescope.
   -- In all later call to insertImplicitPatterns, we can then use ExpandLast.
-  ps <- insertImplicitPatternsT DontExpandLast ps a
+  -- Ulf, 2016-04-25: Actually we do need to ExpandLast because where blocks
+  -- need the implicits.
+  ps <- insertImplicitPatternsT ExpandLast ps a
   -- unless (size tel0' >= size ps) $ typeError $ TooManyArgumentsInLHS a
 
   -- Redo the telView, in order to *not* normalize the clause type further than necessary.
@@ -87,7 +95,7 @@ problemFromPats ps a = do
       pr        = ProblemRest ps2 $ defaultArg b
 
       -- internal patterns start as all variables
-  let ips = teleNamedArgs gamma
+  let ips = teleNamedArgs gamma `useOriginFrom` ps
 
       -- the initial problem for starting the splitting
       problem  = Problem ps1 ips gamma pr :: Problem
@@ -101,7 +109,7 @@ problemFromPats ps a = do
         -- , text "ips   =" <+> prettyTCM ips  -- no prettyTCM instance
            , text "gamma =" <+> prettyTCM gamma
            , text "ps2   =" <+> fsep (map prettyA ps2)
-           , text "b     =" <+> addCtxTel gamma (prettyTCM b)
+           , text "b     =" <+> addContext gamma (prettyTCM b)
            ]
          ]
   return problem
@@ -110,7 +118,7 @@ problemFromPats ps a = do
 --   Possible if type of problem rest has been updated to a function type.
 updateProblemRest_ :: Problem -> TCM (Nat, Problem)
 updateProblemRest_ p@(Problem ps0 qs0 tel0 (ProblemRest ps a)) = do
-      ps <- insertImplicitPatternsT DontExpandLast ps $ unArg a
+      ps <- insertImplicitPatternsT ExpandLast ps $ unArg a
       -- (Issue 734: Do only the necessary telView to preserve clause types as much as possible.)
       TelV tel b   <- telViewUpTo (length ps) $ unArg a
       let gamma     = useNamesFromPattern ps tel
@@ -118,9 +126,9 @@ updateProblemRest_ p@(Problem ps0 qs0 tel0 (ProblemRest ps a)) = do
           (ps1,ps2) = splitAt (size as) ps
           tel1      = telFromList $ telToList tel0 ++ as
           pr        = ProblemRest ps2 (a $> b)
-          qs1       = teleNamedArgs gamma
+          qs1       = teleNamedArgs gamma `useOriginFrom` ps
           n         = size as
-      reportSDoc "tc.lhs.problem" 10 $ addCtxTel tel0 $ vcat
+      reportSDoc "tc.lhs.problem" 10 $ addContext tel0 $ vcat
         [ text "checking lhs -- updated split problem:"
         , nest 2 $ vcat
           [ text "ps    =" <+> fsep (map prettyA ps)
@@ -129,7 +137,7 @@ updateProblemRest_ p@(Problem ps0 qs0 tel0 (ProblemRest ps a)) = do
           , text "ps1   =" <+> fsep (map prettyA ps1)
           , text "gamma =" <+> prettyTCM gamma
           , text "ps2   =" <+> fsep (map prettyA ps2)
-          , text "b     =" <+> addCtxTel gamma (prettyTCM b)
+          , text "b     =" <+> addContext gamma (prettyTCM b)
           ]
         ]
       return $ (n,) $ Problem (ps0 ++ ps1) (applySubst (raiseS n) qs0 ++ qs1) tel1 pr
@@ -141,7 +149,5 @@ updateProblemRest st@LHSState { lhsProblem = p } = do
     let tau = raiseS n
     return $ LHSState
       { lhsProblem = p'
-      , lhsSubst   = applySubst tau (lhsSubst st)
       , lhsDPI     = applyPatSubst tau (lhsDPI st)
-      , lhsAsB     = applyPatSubst tau (lhsAsB st)
       }