@@ -262,20 +262,67 @@ irTerm vs env tm@(App f a) = case unApply tm of
262262 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
263263 ])
264264
265+ -- data constructor
265266 (P (DCon t arity) n _, args) -> do
266267 detag <- fgetState (opt_detaggable . ist_optimisation n)
267268 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
268269
269− when (length args > arity) $
270− ifail ("oversaturated data ctor: " ++ show tm)
271−
272− let args' = [a | (i,a) <- zip [0..] args, i `elem` used]
273− if length args' == 1 && detag -- detaggable
274− then irTerm vs env (head args') -- newtype
275− else irCon vs env (length used) n args'
276−
270+ let isNewtype = length used == 1 && detag
271+ let argsPruned = [a | (i,a) <- zip [0..] args, i `elem` used]
272+
273+ -- The following code removes fields from data constructors
274+ -- and performs the newtype optimisation.
275+ --
276+ -- The general rule here is:
277+ -- Everything we get as input is not touched by erasure,
278+ -- so it conforms to the official arities and types
279+ -- and we can reason about it like it's plain TT.
280+ --
281+ -- It's only the data that leaves this point that's erased
282+ -- and possibly no longer typed as the original TT version.
283+ --
284+ -- Especially, underapplied constructors must yield functions
285+ -- even if all the remaining arguments are erased
286+ -- (the resulting function *will* be applied, to NULLs).
287+ --
288+ -- This will probably need rethinking when we get erasure from functions.
289+
290+ -- "padLams" will wrap our term in LLam-bdas and give us
291+ -- the "list of future unerased args" coming from these lambdas.
292+ --
293+ -- We can do whatever we like with the list of unerased args,
294+ -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.
295+ let padLams = padLambdas used (length args) arity
296+
297+ case compare arity (length args) of
298+
299+ -- overapplied
300+ GT -> ifail ("overapplied data constructor: " ++ show tm)
301+
302+ -- exactly saturated
303+ EQ | isNewtype
304+ -> irTerm vs env (head argsPruned)
305+
306+ | otherwise -- not newtype, plain data ctor
307+ -> buildApp (LV $ Glob n) argsPruned
308+
309+ -- not saturated, underapplied
310+ LT | isNewtype -- newtype
311+ , length argsPruned == 1 -- and we already have the value
312+ -> padLams . (\tm [] -> tm) -- the [] asserts there are no unerased args
313+ <$> irTerm vs env (head argsPruned)
314+
315+ | isNewtype -- newtype but the value is not among args yet
316+ -> return . padLams $ \[vn] -> LApp False (LV $ Glob n) [LV $ Glob vn]
317+
318+ -- not a newtype, just apply to a constructor
319+ | otherwise
320+ -> padLams . applyToNames <$> buildApp (LV $ Glob n) argsPruned
321+
322+ -- type constructor
277323 (P (TCon t a) n _, args) -> return LNothing
278324
325+ -- a name applied to arguments
279326 (P _ n _, args) -> do
280327 ist <- getIState
281328 case lookup n (idris_scprims ist) of
@@ -296,9 +343,24 @@ irTerm vs env tm@(App f a) = case unApply tm of
296343 <*> mapM (irTerm vs env) args
297344
298345 where
346+ buildApp :: LExp -> [Term] -> Idris LExp
347+ buildApp e [] = return e
348+ buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
349+
350+ applyToNames :: LExp -> [Name] -> LExp
351+ applyToNames tm [] = tm
352+ applyToNames tm ns = LApp False tm $ map (LV . Glob) ns
353+
354+ padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
355+ padLambdas used startIdx endSIdx mkTerm
356+ = LLam allNames $ mkTerm nonerasedNames
357+ where
358+ allNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1]]
359+ nonerasedNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1], i `elem` used]
360+
299361 applyName :: Name -> IState -> [Term] -> Idris LExp
300362 applyName n ist args =
301− LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
363+ LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
302364 where
303365 erase (i, x)
304366 | i >= arity || i `elem` used = x
@@ -345,24 +407,6 @@ irTerm vs env (TType _) = return $ LNothing
345407irTerm vs env Erased = return $ LNothing
346408irTerm vs env Impossible = return $ LNothing
347409
348−irCon :: Vars -> [Name] -> Int -> Name -> [Term] -> Idris LExp
349−irCon vs env arity n args
350− | length args > arity
351− = error $ "oversaturated data constructor: " ++ show (n, args)
352−
353− -- saturated
354− | length args == arity
355− = buildApp (LV (Glob n)) args
356−
357− -- undersaturated, wrap in lambdas
358− | otherwise
359− = let extraNs = [sMN i "sat" | i <- [length args .. arity-1]]
360− extraTs = [P Bound n undefined | n <- extraNs]
361− in LLam extraNs <$> irCon vs env arity n (args ++ extraTs)
362− where
363− buildApp e [] = return e
364− buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
365−
366410doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp
367411doForeign vs env (_ : fgn : args)
368412 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn