summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/DropArgs.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/DropArgs.hs')
-rw-r--r--src/full/Agda/TypeChecking/DropArgs.hs19
1 files changed, 6 insertions, 13 deletions
diff --git a/src/full/Agda/TypeChecking/DropArgs.hs b/src/full/Agda/TypeChecking/DropArgs.hs
index 7a87a67..9cb42c2 100644
--- a/src/full/Agda/TypeChecking/DropArgs.hs
+++ b/src/full/Agda/TypeChecking/DropArgs.hs
@@ -1,5 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
module Agda.TypeChecking.DropArgs where
@@ -8,7 +7,6 @@ import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
-import Agda.TypeChecking.Substitute.Pattern
import Agda.TypeChecking.CompiledClause
@@ -37,22 +35,17 @@ instance DropArgs Telescope where
instance DropArgs Permutation where
dropArgs n (Perm m p) = Perm (m - n) $ map (subtract n) $ drop n p
--- | NOTE: does not go into the body, so does not work for recursive functions.
-instance DropArgs ClauseBody where
- dropArgs 0 b = b
- dropArgs _ NoBody = NoBody
- dropArgs n (Bind b) = dropArgs (n - 1) (absBody b)
- dropArgs n Body{} = __IMPOSSIBLE__
-
-- | NOTE: does not work for recursive functions.
instance DropArgs Clause where
dropArgs n cl =
- cl{ clauseTel = dropArgs n $ clauseTel cl
- -- Andreas, 2012-09-25: just dropping the front of telescope
+ cl{ -- Andreas, 2012-09-25: just dropping the front of telescope
-- makes it ill-formed (unbound indices)
-- we should let the telescope intact!?
- , namedClausePats = drop n $ namedClausePats cl
- , clauseBody = dropArgs n $ clauseBody cl -- BUG: need to drop also from recursive calls!!
+ -- Ulf, 2016-06-23: Indeed. After parameter refinement it's even
+ -- worse: the module parameters we want to drop aren't necessarily
+ -- the first things in the telescope.
+ namedClausePats = drop n $ namedClausePats cl
+ -- BUG: need to drop also from recursive calls!!
}
instance DropArgs FunctionInverse where