@@ -76,12 +76,12 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
7676 ctxt <- getContext
7777 i <- getIState
7878
79− logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'
79+ logLvl 1 $ show n ++ " pre-type " ++ showTmImpls ty'
8080 ty' <- addUsingConstraints syn fc ty'
8181 ty' <- implicit syn n ty'
8282
8383 let ty = addImpl i ty'
84− logLvl 2 $ show n ++ " type " ++ showTmImpls ty
84+ logLvl 1 $ show n ++ " type " ++ showTmImpls ty
8585 ((tyT, defer, is), log) <-
8686 tclift $ elaborate ctxt n (TType (UVal 0)) []
8787 (errAt "type of " n (erun fc (build i info False [] n ty)))
@@ -662,7 +662,7 @@ elabProvider info syn fc n ty tm
662662 tm <- getProvided fc rhs'
663663
664664 -- Finally add a top-level definition of the provided term
665− elabClauses info fc [] n [PClause fc n (PRef fc n) [] (delab i tm) []]
665+ elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]
666666 logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
667667
668668 where isTType :: TT Name -> Bool
@@ -1266,6 +1266,68 @@ checkPossible info fc tcgen fname lhs_in
12661266 ((P _ x _, _), (P _ y _, _)) -> x == y
12671267 _ -> False
12681268
1269+getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)
1270+ = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
1271+getFixedInType i env (_ : is) (Bind n (Pi t) sc)
1272+ = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
1273+getFixedInType i env is tm@(App f a)
1274+ | (P _ tn _, args) <- unApply tm
1275+ = case lookupCtxt tn (idris_datatypes i) of
1276+ [t] -> nub $ paramNames args env (param_pos t) ++
1277+ getFixedInType i env is f ++
1278+ getFixedInType i env is a
1279+ [] -> nub $ getFixedInType i env is f ++
1280+ getFixedInType i env is a
1281+ | otherwise = nub $ getFixedInType i env is f ++
1282+ getFixedInType i env is a
1283+getFixedInType i _ _ _ = []
1284+
1285+getFlexInType i env (Bind n (Pi t) sc)
1286+ = nub $ getFlexInType i env t ++
1287+ getFlexInType i (n : env) (instantiate (P Bound n t) sc)
1288+getFlexInType i env tm@(App f a)
1289+ | (P _ tn _, args) <- unApply tm
1290+ = case lookupCtxt tn (idris_datatypes i) of
1291+ [t] -> nub $ paramNames args env [x | x <- [0..length args],
1292+ not (x `elem` param_pos t)]
1293+ ++ getFlexInType i env f ++
1294+ getFlexInType i env a
1295+ [] -> nub $ getFlexInType i env f ++
1296+ getFlexInType i env a
1297+ | otherwise = nub $ getFlexInType i env f ++
1298+ getFlexInType i env a
1299+getFlexInType i _ _ = []
1300+
1301+-- Treat a name as a parameter if it appears in parameter positions in
1302+-- types, and never in a non-parameter position in a type.
1303+
1304+getParamsInType i env ps t = let fix = getFixedInType i env ps t
1305+ flex = getFlexInType i env t in
1306+ [x | x <- fix, not (x `elem` flex)]
1307+
1308+paramNames args env [] = []
1309+paramNames args env (p : ps)
1310+ | length args > p = case args!!p of
1311+ P _ n _ -> if n `elem` env
1312+ then n : paramNames args env ps
1313+ else paramNames args env ps
1314+ _ -> paramNames args env ps
1315+ | otherwise = paramNames args env ps
1316+
1317+propagateParams :: [Name] -> Type -> PTerm -> PTerm
1318+propagateParams ps t tm@(PApp _ (PRef fc n) args)
1319+ = PApp fc (PRef fc n) (addP t args)
1320+ where addP (Bind n _ sc) (t : ts)
1321+ | Placeholder <- getTm t,
1322+ n `elem` ps,
1323+ not (n `elem` allNamesIn tm)
1324+ = t { getTm = PRef fc n } : addP sc ts
1325+ addP (Bind n _ sc) (t : ts) = t : addP sc ts
1326+ addP _ ts = ts
1327+propagateParams ps t (PRef fc n)
1328+ = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)
1329+propagateParams ps t x = x
1330+
12691331elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
12701332 Idris (Either Term (Term, Term))
12711333elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
@@ -1292,10 +1354,12 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
12921354 [t] -> t
12931355 _ -> []
12941356 let params = getParamsInType i [] fn_is fn_ty
1295− let lhs = stripUnmatchable i $
1296− addImplPat i (propagateParams params (stripLinear i lhs_in))
1297− logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)
1298− logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
1357+ let flex = getFlexInType i [] fn_ty
1358+ let lhs = mkLHSapp $ stripUnmatchable i $
1359+ propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))
1360+ logLvl 5 ("LHS: " ++ show fc ++ " " ++ show lhs)
1361+ logLvl 4 ("Fixed parameters: " ++ show (flex, params) ++ " from " ++ show lhs_in ++
1362+ "\n" ++ show (fn_ty, fn_is))
12991363
13001364 (((lhs', dlhs, []), probs, inj), _) <-
13011365 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
@@ -1342,7 +1406,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
13421406 -- Elaborate those with a type *before* RHS, those without *after*
13431407 let (wbefore, wafter) = sepBlocks wb
13441408
1345− logLvl 5 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
1409+ logLvl 1 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
13461410 mapM_ (elabDecl' EAll info) wbefore
13471411 -- Now build the RHS, using the type of the LHS as the goal.
13481412 i <- getIState -- new implicits from where block
@@ -1355,7 +1419,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
13551419 ((rhs', defer, is, probs), _) <-
13561420 tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []
13571421 (do pbinds ist lhs_tm
1358− mapM_ setinj inj
1422+ mapM_ setinj (nub (params ++ inj))
13591423 setNextName
13601424 (_, _, is) <- errAt "right hand side of " fname
13611425 (erun fc (build i info False opts fname rhs))
@@ -1415,6 +1479,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
14151479 addErrRev (crhs, clhs)
14161480 return $ Right (clhs, crhs)
14171481 where
1482+ mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []
1483+ mkLHSapp t = t
1484+
14181485 decorate (NS x ns)
14191486 = NS (SN (WhereN cnum fname x)) ns -- ++ [show cnum])
14201487-- = NS (UN ('#':show x)) (ns ++ [show cnum, show fname])
@@ -1447,40 +1514,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
14471514 -- _ -> MN i (show n)) . l
14481515 }
14491516
1450− getParamsInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)
1451− = getParamsInType i env is (instantiate (P Bound n t) sc)
1452− getParamsInType i env (_ : is) (Bind n (Pi t) sc)
1453− = getParamsInType i (n : env) is (instantiate (P Bound n t) sc)
1454− getParamsInType i env is tm@(App f a)
1455− | (P _ tn _, args) <- unApply tm
1456− = case lookupCtxt tn (idris_datatypes i) of
1457− [t] -> nub $ paramNames args env (param_pos t) ++
1458− getParamsInType i env is f ++
1459− getParamsInType i env is a
1460− [] -> nub $ getParamsInType i env is f ++
1461− getParamsInType i env is a
1462− | otherwise = nub $ getParamsInType i env is f ++
1463− getParamsInType i env is a
1464− getParamsInType i _ _ _ = []
1465−
1466− paramNames args env [] = []
1467− paramNames args env (p : ps)
1468− | length args > p = case args!!p of
1469− P _ n _ -> if n `elem` env
1470− then n : paramNames args env ps
1471− else paramNames args env ps
1472− _ -> paramNames args env ps
1473− | otherwise = paramNames args env ps
1474−
1475− propagateParams :: [Name] -> PTerm -> PTerm
1476− propagateParams ps (PApp _ (PRef fc n) args)
1477− = PApp fc (PRef fc n) (map addP args)
1478− where addP imp@(PImp _ _ _ _ Placeholder _)
1479− | pname imp `elem` ps = imp { getTm = PRef fc (pname imp) }
1480− addP t = t
1481− propagateParams ps (PRef fc n)
1482− = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)
1483− propagateParams ps x = x
14841517
14851518 -- if a hole is just an argument/result of a case block, treat it as
14861519 -- the unit type. Hack to help elaborate case in do blocks.
@@ -1508,8 +1541,16 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
15081541 -- Build the LHS as an "Infer", and pull out its type and
15091542 -- pattern bindings
15101543 i <- getIState
1511− let lhs = addImplPat i (stripLinear i lhs_in)
1512− logLvl 5 ("LHS: " ++ showTmImpls lhs)
1544+ -- get the parameters first, to pass through to any where block
1545+ let fn_ty = case lookupTy fname (tt_ctxt i) of
1546+ [t] -> t
1547+ _ -> error "Can't happen (elabClause function type)"
1548+ let fn_is = case lookupCtxt fname (idris_implicits i) of
1549+ [t] -> t
1550+ _ -> []
1551+ let params = getParamsInType i [] fn_is fn_ty
1552+ let lhs = propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))
1553+ logLvl 1 ("LHS: " ++ show lhs)
15131554 ((lhs', dlhs, []), _) <-
15141555 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
15151556 (errAt "left hand side of with in " fname