ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-15 01:25:05 +03:00
Code Issues Projects Releases Wiki Activity

Merge remote-tracking branch 'refs/remotes/upstream/master' into ahmadsalim-testing/cstaticanalysis

Browse Source
This commit is contained in:
David Raymond Christiansen 2015-03-19 20:46:24 +01:00
commit 5ed857b100
36 changed files with 196 additions and 116 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
CHANGELOG
View File

@ -40,6 +40,8 @@ New in 0.9.17:
* Classes can now be annotated with 'determining parameters' to say which
must be available before resolving instances. Only determining parameters
are checked when checking for overlapping instances.
* Arguments to class instances are now checked for injectivity.
Unification assumes this, so we need to check when instances are defined.
New in 0.9.16:
--------------

3
idris.cabal
View File

@ -289,6 +289,9 @@ Extra-source-files:
test/reg058/run
test/reg058/*.idr
test/reg058/expected
test/reg059/run
test/reg059/*.idr
test/reg059/expected
test/basic001/run
test/basic001/*.idr

1
libs/base/Language/Reflection/Utils.idr
View File

@ -270,6 +270,7 @@ instance Show Err where
show (NoTypeDecl n) = "NoTypeDecl " ++ show n
show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'
show (CantResolve tm) = "CantResolve " ++ show tm
show (InvalidTCArg n tm) = "InvalidTCName " ++ show n ++ " (" ++ show tm ++ ")"
show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs
show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm
show (NoEliminator s tm) = "NoEliminator " ++ show s ++ " " ++ show tm

1
libs/prelude/Language/Reflection/Errors.idr
View File

@ -29,6 +29,7 @@ data Err = Msg String
| NoTypeDecl TTName
| NotInjective TT TT TT
| CantResolve TT
| InvalidTCArg TTName TT
| CantResolveAlts (List TTName)
| IncompleteTerm TT
| NoEliminator String TT

4
libs/prelude/Prelude/Applicative.idr
View File

@ -15,10 +15,6 @@ class Functor f => Applicative (f : Type -> Type) where
pure : a -> f a
(<*>) : f (a -> b) -> f a -> f b
instance Applicative id where
pure a = a
f <*> a = f a
class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
applicativeMap : (x : f a) -> (g : a -> b) ->
map g x = pure g <*> x

2
libs/prelude/Prelude/Functor.idr
View File

@ -24,5 +24,3 @@ class Functor f => VerifiedFunctor (f : Type -> Type) where
(g1 : a -> b) -> (g2 : b -> c) ->
map (g2 . g1) x = (map g2 . map g1) x
instance Functor id where
map f a = f a

3
libs/prelude/Prelude/Monad.idr
View File

@ -24,9 +24,6 @@ class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
(mx >>= f) >>= g = mx >>= (\x => f x >>= g)
instance Monad id where
a >>= f = f a
||| Also called `join` or mu
flatten : Monad m => m (m a) -> m a
flatten a = a >>= id

17
rts/idris_gc.c
View File

@ -112,19 +112,8 @@ void idris_gc(VM* vm) {
if (vm->heap.old != NULL)
free(vm->heap.old);
char* newheap = malloc(vm->heap.size);
char* oldheap = vm->heap.heap;
vm->heap.heap = newheap;
#ifdef FORCE_ALIGNMENT
if (((i_int)(vm->heap.heap)&1) == 1) {
vm->heap.next = newheap + 1;
} else
#endif
{
vm->heap.next = newheap;
}
vm->heap.end = newheap + vm->heap.size;
/* Allocate swap heap. */
alloc_heap(&vm->heap, vm->heap.size, vm->heap.growth, vm->heap.heap);
VAL* root;
@ -139,6 +128,7 @@ void idris_gc(VM* vm) {
msg->msg = copy(vm, msg->msg);
}
#endif
vm->ret = copy(vm, vm->ret);
vm->reg1 = copy(vm, vm->reg1);
@ -150,7 +140,6 @@ void idris_gc(VM* vm) {
if ((vm->heap.next - vm->heap.heap) > vm->heap.size >> 1) {
vm->heap.size += vm->heap.growth;
}
vm->heap.old = oldheap;
STATS_LEAVE_GC(vm->stats, vm->heap.size, vm->heap.next - vm->heap.heap)
HEAP_CHECK(vm)

9
rts/idris_heap.c
View File

@ -5,7 +5,9 @@
#include <stddef.h>
#include <stdio.h>
void alloc_heap(Heap * h, size_t heap_size)
/* Used for initializing the heap. */
void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old)
{
char * mem = malloc(heap_size);
if (mem == NULL) {
@ -27,9 +29,9 @@ void alloc_heap(Heap * h, size_t heap_size)
h->end = h->heap + heap_size;
h->size = heap_size;
h->growth = heap_size;
h->growth = growth;
h->old = NULL;
h->old = old;
}
void free_heap(Heap * h) {
@ -40,6 +42,7 @@ void free_heap(Heap * h) {
}
}
// TODO: more testing
/******************** Heap testing ********************************************/
void heap_check_underflow(Heap * heap) {

2
rts/idris_heap.h
View File

@ -14,7 +14,7 @@ typedef struct {
} Heap;
void alloc_heap(Heap * heap, size_t heap_size);
void alloc_heap(Heap * heap, size_t heap_size, size_t growth, char * old);
void free_heap(Heap * heap);

2
rts/idris_rts.c
View File

@ -29,7 +29,7 @@ VM* init_vm(int stack_size, size_t heap_size,
vm->valstack_base = valstack;
vm->stack_max = valstack + stack_size;
alloc_heap(&(vm->heap), heap_size);
alloc_heap(&(vm->heap), heap_size, heap_size, NULL);
vm->ret = NULL;
vm->reg1 = NULL;

46
src/Idris/AbsSyntax.hs
View File

@ -1481,31 +1481,34 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
-- Add implicit arguments in function calls
addImplPat :: IState -> PTerm -> PTerm
addImplPat = addImpl' True [] []
addImplPat = addImpl' True [] [] []
addImplBound :: IState -> [Name] -> PTerm -> PTerm
addImplBound ist ns = addImpl' False ns [] ist
addImplBound ist ns = addImpl' False ns [] [] ist
addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
addImplBoundInf ist ns inf = addImpl' False ns inf ist
addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
-- | Add the implicit arguments to applications in the term
addImpl :: IState -> PTerm -> PTerm
-- [Name] gives the names to always expend, even when under a binder of
-- that name (this is to expand methods with implicit arguments in dependent
-- type classes).
addImpl :: [Name] -> IState -> PTerm -> PTerm
addImpl = addImpl' False [] []
-- TODO: in patterns, don't add implicits to function names guarded by constructors
-- and *not* inside a PHidden
addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
addImpl' inpat env infns ist ptm
addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
addImpl' inpat env infns imp_meths ist ptm
= mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
where
ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
ai qq env ds (PRef fc f)
| f `elem` infns = PInferRef fc f
| not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []
| not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq imp_meths ist fc f ds []
ai qq env ds (PHidden (PRef fc f))
| not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq ist fc f ds [])
| not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq imp_meths ist fc f ds [])
ai qq env ds (PEq fc lt rt l r)
= let lt' = ai qq env ds lt
rt' = ai qq env ds rt
@ -1541,7 +1544,7 @@ addImpl' inpat env infns ist ptm
| f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
| not (f `elem` map fst env)
= let as' = map (fmap (ai qq env ds)) as in
handleErr $ aiFn inpat False qq ist fc f ds as'
handleErr $ aiFn inpat False qq imp_meths ist fc f ds as'
| Just (Just ty) <- lookup f env =
let as' = map (fmap (ai qq env ds)) as
arity = getPArity ty in
@ -1576,7 +1579,9 @@ addImpl' inpat env infns ist ptm
_ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])
ai qq env ds (PPi p n ty sc)
= let ty' = ai qq env ds ty
sc' = ai qq ((n, Just ty):env) ds sc in
env' = if n `elem` imp_meths then env
else ((n, Just ty) : env)
sc' = ai qq env' ds sc in
PPi p n ty' sc'
ai qq env ds (PGoal fc r n sc)
= let r' = ai qq env ds r
@ -1600,8 +1605,8 @@ addImpl' inpat env infns ist ptm
-- if in a pattern, and there are no arguments, and there's no possible
-- names with zero explicit arguments, don't add implicits.
aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
aiFn inpat True qq ist fc f ds []
aiFn :: Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
aiFn inpat True qq imp_meths ist fc f ds []
= case lookupDef f (tt_ctxt ist) of
[] -> Right $ PPatvar fc f
alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
@ -1609,7 +1614,7 @@ aiFn inpat True qq ist fc f ds []
if (not (vname f) || tcname f
|| any (conCaf (tt_ctxt ist)) ialts)
-- any constructor alts || any allImp ialts))
then aiFn inpat False qq ist fc f ds [] -- use it as a constructor
then aiFn inpat False qq imp_meths ist fc f ds [] -- use it as a constructor
else Right $ PPatvar fc f
where imp (PExp _ _ _ _) = False
imp _ = True
@ -1623,9 +1628,9 @@ aiFn inpat True qq ist fc f ds []
vname (UN n) = True -- non qualified
vname _ = False
aiFn inpat expat qq ist fc f ds as
aiFn inpat expat qq imp_meths ist fc f ds as
| f `elem` primNames = Right $ PApp fc (PRef fc f) as
aiFn inpat expat qq ist fc f ds as
aiFn inpat expat qq imp_meths ist fc f ds as
-- This is where namespaces get resolved by adding PAlternative
= do let ns = lookupCtxtName f (idris_implicits ist)
let nh = filter (\(n, _) -> notHidden n) ns
@ -1633,15 +1638,20 @@ aiFn inpat expat qq ist fc f ds as
[] -> nh
x -> x
case ns' of
[(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
[(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc (isImpName f f')) (insertImpl ns as)
[] -> if f `elem` (map fst (idris_metavars ist))
then Right $ PApp fc (PRef fc f) as
else Right $ mkPApp fc (length as) (PRef fc f) as
alts -> Right $
PAlternative True $
map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
map (\(f', ns) -> mkPApp fc (length ns) (PRef fc (isImpName f f'))
(insertImpl ns as)) alts
where
-- if the name is in imp_meths, we should actually refer to the bound
-- name rather than the global one after expanding implicits
isImpName f f' | f `elem` imp_meths = f
| otherwise = f'
trimAlts [] alts = alts
trimAlts ns alts
= filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
@ -1685,7 +1695,7 @@ aiFn inpat expat qq ist fc f ds as
PImp p True l n Placeholder :
insImpAcc (M.insert n Placeholder pnas) ps given imps
insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
let sc = addImpl ist (substMatches (M.toList pnas) sc') in
let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
case find n imps [] of
Just (tm, imps') ->
PTacImplicit p l n sc tm :

5
src/Idris/AbsSyntaxTree.hs
View File

@ -1198,6 +1198,9 @@ data SyntaxInfo = Syn { using :: [Using],
syn_params :: [(Name, PTerm)],
syn_namespace :: [String],
no_imp :: [Name],
imp_methods :: [Name], -- class methods. When expanding
-- implicits, these should be expanded even under
-- binders
decoration :: Name -> Name,
inPattern :: Bool,
implicitAllowed :: Bool,
@ -1211,7 +1214,7 @@ deriving instance NFData SyntaxInfo
deriving instance Binary SyntaxInfo
!-}
defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0
defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0
expandNS :: SyntaxInfo -> Name -> Name
expandNS syn n@(NS _ _) = n

6
src/Idris/Core/Binary.hs
View File

@ -149,6 +149,9 @@ instance Binary a => Binary (Err' a) where
put (NoEliminator s t) = do putWord8 37
put s
put t
put (InvalidTCArg n t) = do putWord8 38
put n
put t
get = do i <- getWord8
case i of
@ -211,6 +214,9 @@ instance Binary a => Binary (Err' a) where
37 -> do x1 <- get
x2 <- get
return (NoEliminator x1 x2)
38 -> do x1 <- get
x2 <- get
return (InvalidTCArg x1 x2)
_ -> error "Corrupted binary data for Err'"
----- Generated by 'derive'

1
src/Idris/Core/DeepSeq.hs
View File

@ -81,6 +81,7 @@ instance NFData Err where
rnf (NotInjective x1 x2 x3)
= rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
rnf (CantResolve x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
rnf (InvalidTCArg x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
rnf (CantResolveAlts x1) = rnf x1 `seq` ()
rnf (IncompleteTerm x1) = rnf x1 `seq` ()
rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

37
src/Idris/Core/TT.hs
View File

@ -157,6 +157,7 @@ data Err' t
| NotInjective t t t
| CantResolve Bool -- True if postponed, False if fatal
t
| InvalidTCArg Name t
| CantResolveAlts [Name]
| IncompleteTerm t
| NoEliminator String t
@ -1170,17 +1171,33 @@ unList tm = case unApply tm of
forget :: TT Name -> Raw
forget tm = forgetEnv [] tm
safeForget :: TT Name -> Maybe Raw
safeForget tm = safeForgetEnv [] tm
forgetEnv :: [Name] -> TT Name -> Raw
forgetEnv env (P _ n _) = Var n
forgetEnv env (V i) = Var (env !! i)
forgetEnv env (Bind n b sc) = let n' = uniqueName n env in
RBind n' (fmap (forgetEnv env) b)
(forgetEnv (n':env) sc)
forgetEnv env (App f a) = RApp (forgetEnv env f) (forgetEnv env a)
forgetEnv env (Constant c) = RConstant c
forgetEnv env (TType i) = RType
forgetEnv env (UType u) = RUType u
forgetEnv env Erased = RConstant Forgot
forgetEnv env tm = case safeForgetEnv env tm of
Just t' -> t'
Nothing -> error $ "Scope error in " ++ show tm
safeForgetEnv :: [Name] -> TT Name -> Maybe Raw
safeForgetEnv env (P _ n _) = Just $ Var n
safeForgetEnv env (V i) | i < length env = Just $ Var (env !! i)
| otherwise = Nothing
safeForgetEnv env (Bind n b sc)
= do let n' = uniqueName n env
b' <- safeForgetEnvB env b
sc' <- safeForgetEnv (n':env) sc
Just $ RBind n' b' sc'
where safeForgetEnvB env (Let t v) = liftM2 Let (safeForgetEnv env t)
(safeForgetEnv env v)
safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)
Just $ fmap (\_ -> ty') b
safeForgetEnv env (App f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)
safeForgetEnv env (Constant c) = Just $ RConstant c
safeForgetEnv env (TType i) = Just RType
safeForgetEnv env (UType u) = Just $ RUType u
safeForgetEnv env Erased = Just $ RConstant Forgot
-- | Introduce a 'Bind' into the given term for each element of the
-- given list of (name, binder) pairs.

2
src/Idris/Coverage.hs
View File

@ -24,7 +24,7 @@ import Control.Monad.State.Strict
-- provided explicitly from new clause generation.
mkPatTm :: PTerm -> Idris Term
mkPatTm t = do i <- getIState
let timp = addImpl' True [] [] i t
let timp = addImpl' True [] [] [] i t
evalStateT (toTT (mapPT deNS timp)) 0
where
toTT (PRef _ n) = do i <- lift getIState

4
src/Idris/DeepSeq.hs
View File

@ -353,10 +353,10 @@ instance NFData Using where
rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
instance NFData SyntaxInfo where
rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)
rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
= rnf x1 `seq`
rnf x2 `seq`
rnf x3 `seq`
rnf x4 `seq`
rnf x5 `seq`
rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()
rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()

4
src/Idris/Delaborate.hs
View File

@ -290,6 +290,10 @@ pprintErr' i (NotInjective p x y) =
text " when unifying" <+> annTm x (pprintTerm i (delab i x)) <+> text "and" <+>
annTm y (pprintTerm i (delab i y))
pprintErr' i (CantResolve _ c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)
pprintErr' i (InvalidTCArg n t)
= annTm t (pprintTerm i (delab i t)) <+> text " cannot be a parameter of "
<> annName n <$>
text "(Type class arguments must be injective)"
pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))
pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

22
src/Idris/Elab/Class.hs
View File

@ -77,28 +77,28 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
= unzip (map (\ ( x,y,z) -> (x, y)) ims)
let defaults = map (\ (x, (y, z)) -> (x,y)) defs
-- build instance constructor type
-- decorate names of functions to ensure they can't be referred
-- to elsewhere in the class declaration
let cty = impbind ps $ conbind constraints
$ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
constraint
let cons = [(emptyDocstring, [], cn, cty, fc, [])]
let ddecl = PDatadecl tn tty cons
logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)
elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl
-- Elaborate the data declaration
elabData info (syn { no_imp = no_imp syn ++ mnames,
imp_methods = mnames }) doc pDocs fc [] ddecl
dets <- findDets cn fds
addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [] dets)
-- for each constraint, build a top level function to chase it
logLvl 5 $ "Building functions"
-- let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps
-- ++ using syn }
fns <- mapM (cfun cn constraint syn (map fst imethods)) constraints
mapM_ (rec_elabDecl info EAll info) (concat fns)
cfns <- mapM (cfun cn constraint syn (map fst imethods)) constraints
mapM_ (rec_elabDecl info EAll info) (concat cfns)
-- for each method, build a top level function
fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods
logLvl 5 $ "Functions " ++ show fns
-- Elaborate the the top level methods
mapM_ (rec_elabDecl info EAll info) (concat fns)
-- add the default definitions
mapM_ (rec_elabDecl info EAll info) (concat (map (snd.snd) defs))
addIBC (IBCClass tn)
@ -134,8 +134,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
getMName (PTy _ _ _ _ _ n _) = nsroot n
tdecl allmeths (PTy doc _ syn _ o n t)
= do t' <- implicit' info syn allmeths n t
logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
= do t' <- implicit' info syn (map fst ps ++ allmeths) n t
logLvl 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
return ( (n, (toExp (map fst ps) Exp t')),
(n, (doc, o, (toExp (map fst ps)
(\ l s p -> Imp l s p Nothing) t'))),

20
src/Idris/Elab/Clause.hs
View File

@ -548,7 +548,7 @@ elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
= do let tcgen = Dictionary `elem` opts
i <- get
let lhs = addImpl i lhs_in
let lhs = addImpl [] i lhs_in
b <- checkPossible info fc tcgen fname lhs_in
case b of
True -> tclift $ tfail (At fc
@ -603,7 +603,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
-- If we're inferring metavariables in the type, don't recheck,
-- because we're only doing this to try to work out those metavariables
(clhs_c, clhsty) <- if not inf
then recheckC fc [] lhs_tm
then recheckC fc id [] lhs_tm
else return (lhs_tm, lhs_ty)
let clhs = normalise ctxt [] clhs_c
let borrowed = borrowedNames [] clhs
@ -681,7 +681,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
logLvl 4 $ "---> " ++ show rhs'
when (not (null defer)) $ iLOG $ "DEFERRED " ++
show (map (\ (n, (_,_,t)) -> (n, t)) defer)
def' <- checkDef fc defer
def' <- checkDef fc (Elaborating "deferred type of ") defer
let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
addDeferred def''
mapM_ (\(n, _) -> addIBC (IBCDef n)) def''
@ -700,7 +700,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
logLvl 6 $ " ==> " ++ show (forget rhs')
(crhs, crhsty) <- if not inf
then recheckC_borrowing True borrowed fc [] rhs'
then recheckC_borrowing True borrowed fc id [] rhs'
else return (rhs', clhsty)
logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty
ctxt <- getContext
@ -828,7 +828,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))
let static_names = getStaticNames i lhs_tm
logLvl 5 (show lhs_tm ++ "\n" ++ show static_names)
(clhs, clhsty) <- recheckC fc [] lhs_tm
(clhs, clhsty) <- recheckC fc id [] lhs_tm
logLvl 5 ("Checked " ++ show clhs)
let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))
let wval = addImplBound i (map fst bargs) wval_in
@ -847,12 +847,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
return (tt, d, is, ctxt', newDecls))
setContext ctxt'
processTacticDecls newDecls
def' <- checkDef fc defer
def' <- checkDef fc iderr defer
let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
addDeferred def''
mapM_ (elabCaseBlock info opts) is
logLvl 5 ("Checked wval " ++ show wval')
(cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
(cwval, cwvalty) <- recheckC fc id [] (getInferTerm wval')
let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)
let cwvalN = explicitNames (normalise ctxt [] cwval)
logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)
@ -907,7 +907,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
addIBC (IBCImp wname)
addIBC (IBCStatic wname)
def' <- checkDef fc [(wname, (-1, Nothing, wtype))]
def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype))]
let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
addDeferred def''
@ -943,12 +943,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
setContext ctxt'
processTacticDecls newDecls
def' <- checkDef fc defer
def' <- checkDef fc iderr defer
let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
addDeferred def''
mapM_ (elabCaseBlock info opts) is
logLvl 5 ("Checked RHS " ++ show rhs')
(crhs, crhsty) <- recheckC fc [] rhs'
(crhs, crhsty) <- recheckC fc id [] rhs'
return $ (Right (clhs, crhs), lhs)
where
getImps (Bind n (Pi _ _ _) t) = pexp Placeholder : getImps t

3
src/Idris/Elab/Data.hs
View File

@ -215,6 +215,7 @@ elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
Idris (Name, Type)
elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
= do checkUndefined fc n
logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in
(cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)
ctxt <- getContext
let cty' = normalise ctxt [] cty
@ -223,7 +224,7 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
-- Check that the constructor type is, in fact, a part of the family being defined
tyIs n cty'
logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
logLvl 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t
logLvl 5 $ "Inaccessible args: " ++ show inacc
logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

31
src/Idris/Elab/Instance.hs
View File

@ -135,6 +135,8 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do
[PClause fc iname lhs [] rhs wb]]
iLOG (show idecls)
mapM_ (rec_elabDecl info EAll info) idecls
ist <- getIState
checkInjectiveArgs fc n (class_determiners ci) (lookupTyExact iname (tt_ctxt ist))
addIBC (IBCInstance intInst n iname)
where
@ -167,7 +169,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do
= do ty' <- addUsingConstraints syn fc t
-- TODO think: something more in info?
ty' <- implicit info syn iname ty'
let ty = addImpl i ty'
let ty = addImpl [] i ty'
ctxt <- getContext
(ElabResult tyT _ _ ctxt' newDecls, _) <-
tclift $ elaborate ctxt iname (TType (UVal 0)) initEState
@ -175,7 +177,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do
setContext ctxt'
processTacticDecls newDecls
ctxt <- getContext
(cty, _) <- recheckC fc [] tyT
(cty, _) <- recheckC fc id [] tyT
let nty = normalise ctxt [] cty
return $ any (isJust . findOverlapping i (class_determiners ci) (delab i nty)) (class_instances ci)
@ -276,3 +278,28 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do
clauseFor m iname ns (PClauses _ _ m' _)
= decorate ns iname m == decorate ns iname m'
clauseFor m iname ns _ = False
checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()
checkInjectiveArgs fc n ds Nothing = return ()
checkInjectiveArgs fc n ds (Just ty)
= do ist <- getIState
let (_, args) = unApply (instantiateRetTy ty)
ci 0 ist args
where
ci i ist (a : as) | i `elem` ds
= if isInj ist a then ci (i + 1) ist as
else tclift $ tfail (At fc (InvalidTCArg n a))
ci i ist (a : as) = ci (i + 1) ist as
ci i ist [] = return ()
isInj i (P Bound n _) = True
isInj i (P _ n _) = isConName n (tt_ctxt i)
isInj i (App f a) = isInj i f && isInj i a
isInj i (V _) = True
isInj i (Bind n b sc) = isInj i sc
isInj _ _ = True
instantiateRetTy (Bind n (Pi _ _ _) sc)
= substV (P Bound n Erased) (instantiateRetTy sc)
instantiateRetTy t = t

4
src/Idris/Elab/Transform.hs
View File

@ -63,7 +63,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
let lhs_ty = getInferType lhs'
let newargs = pvars i lhs_tm
(clhs_tm_in, clhs_ty) <- recheckC fc [] lhs_tm
(clhs_tm_in, clhs_ty) <- recheckC fc id [] lhs_tm
let clhs_tm = renamepats pnames clhs_tm_in
logLvl 3 ("Transform LHS " ++ show clhs_tm)
@ -80,7 +80,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
setContext ctxt'
processTacticDecls newDecls
(crhs_tm_in, crhs_ty) <- recheckC fc [] rhs'
(crhs_tm_in, crhs_ty) <- recheckC fc id [] rhs'
let crhs_tm = renamepats pnames crhs_tm_in
logLvl 3 ("Transform RHS " ++ show crhs_tm)

14
src/Idris/Elab/Type.hs
View File

@ -57,13 +57,13 @@ buildType info syn fc opts n ty' = do
ctxt <- getContext
i <- getIState
logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'
logLvl 2 $ show n ++ " pre-type " ++ showTmImpls ty' ++ show (no_imp syn)
ty' <- addUsingConstraints syn fc ty'
ty' <- addUsingImpls syn n fc ty'
let ty = addImpl i ty'
let ty = addImpl (imp_methods syn) i ty'
logLvl 3 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'
logLvl 3 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty
logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'
logLvl 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty
(ElabResult tyT' defer is ctxt' newDecls, log) <-
tclift $ elaborate ctxt n (TType (UVal 0)) initEState
@ -75,7 +75,7 @@ buildType info syn fc opts n ty' = do
logLvl 3 $ show ty ++ "\nElaborated: " ++ show tyT'
ds <- checkAddDef True False fc defer
ds <- checkAddDef True False fc iderr defer
-- if the type is not complete, note that we'll need to infer
-- things later (for solving metavariables)
when (not (null ds)) $ addTyInferred n
@ -85,7 +85,7 @@ buildType info syn fc opts n ty' = do
logLvl 5 $ "Rechecking"
logLvl 6 $ show tyT
logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT
(cty, ckind) <- recheckC fc [] tyT
(cty, ckind) <- recheckC fc id [] tyT
-- record the implicit and inaccessible arguments
i <- getIState
@ -154,7 +154,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
-- Productivity checking now via checking for guarded 'Delay'
let opts' = opts -- if corec then (Coinductive : opts) else opts
let usety = if norm then nty' else nty
ds <- checkDef fc [(n, (-1, Nothing, usety))]
ds <- checkDef fc iderr [(n, (-1, Nothing, usety))]
addIBC (IBCDef n)
let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
addDeferred ds'

28
src/Idris/Elab/Utils.hs
View File

@ -24,30 +24,36 @@ import qualified Data.Map as Map
recheckC = recheckC_borrowing False []
recheckC_borrowing uniq_check bs fc env t
recheckC_borrowing uniq_check bs fc mkerr env t
= do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
ctxt <- getContext
(tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env (forget t) t of
Error e -> tfail (At fc e)
t' <- case safeForget t of
Just ft -> return ft
Nothing -> tclift $ tfail $ mkerr (At fc (IncompleteTerm t))
(tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env t' t of
Error e -> tfail (At fc (mkerr e))
OK x -> return x
logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs
addConstraints fc cs
return (tm, ty)
checkDef :: FC -> [(Name, (Int, Maybe Name, Type))]
-> Idris [(Name, (Int, Maybe Name, Type))]
checkDef fc ns = checkAddDef False True fc ns
iderr :: Name -> Err -> Err
iderr _ e = e
checkAddDef :: Bool -> Bool -> FC
checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))]
-> Idris [(Name, (Int, Maybe Name, Type))]
checkDef fc mkerr ns = checkAddDef False True fc mkerr ns
checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)
-> [(Name, (Int, Maybe Name, Type))]
-> Idris [(Name, (Int, Maybe Name, Type))]
checkAddDef add toplvl fc [] = return []
checkAddDef add toplvl fc ((n, (i, top, t)) : ns)
checkAddDef add toplvl fc mkerr [] = return []
checkAddDef add toplvl fc mkerr ((n, (i, top, t)) : ns)
= do ctxt <- getContext
(t', _) <- recheckC fc [] t
(t', _) <- recheckC fc (mkerr n) [] t
when add $ do addDeferred [(n, (i, top, t, toplvl))]
addIBC (IBCDef n)
ns' <- checkAddDef add toplvl fc ns
ns' <- checkAddDef add toplvl fc mkerr ns
return ((n, (i, top, t')) : ns')
-- | Get the list of (index, name) of inaccessible arguments from an elaborated

6
src/Idris/Elab/Value.hs
View File

@ -56,7 +56,7 @@ elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Nam
elabValBind info aspat norm tm_in
= do ctxt <- getContext
i <- getIState
let tm = addImpl i tm_in
let tm = addImpl [] i tm_in
logLvl 10 (showTmImpls tm)
-- try:
-- * ordinary elaboration
@ -73,13 +73,13 @@ elabValBind info aspat norm tm_in
let vtm = orderPats (getInferTerm tm')
def' <- checkDef (fileFC "(input)") defer
def' <- checkDef (fileFC "(input)") iderr defer
let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
addDeferred def''
mapM_ (elabCaseBlock info []) is
logLvl 3 ("Value: " ++ show vtm)
(vtm_in, vty) <- recheckC (fileFC "(input)") [] vtm
(vtm_in, vty) <- recheckC (fileFC "(input)") id [] vtm
let vtm = if norm then normalise (tt_ctxt i) [] vtm_in
else vtm_in

8
src/Idris/ElabTerm.hs
View File

@ -57,7 +57,7 @@ processTacticDecls info =
updateIState $ \i -> i { idris_implicits =
addDef n impls (idris_implicits i) }
addIBC (IBCImp n)
ds <- checkDef fc [(n, (-1, Nothing, ty))]
ds <- checkDef fc iderr [(n, (-1, Nothing, ty))]
addIBC (IBCDef n)
let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
addDeferred ds'
@ -1375,9 +1375,12 @@ findInstances :: IState -> Term -> [Name]
findInstances ist t
| (P _ n _, _) <- unApply t
= case lookupCtxt n (idris_classes ist) of
[CI _ _ _ _ _ ins _] -> ins
[CI _ _ _ _ _ ins _] -> filter accessible ins
_ -> []
| otherwise = []
where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of
Just (_, Hidden) -> False
_ -> True
-- Try again to solve auto implicits
solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()
@ -2708,6 +2711,7 @@ reflectErr (NotInjective t1 t2 t3) =
, reflect t3
]
reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]
reflectErr (CantResolveAlts ss) =
raw_apply (Var $ reflErrName "CantResolveAlts")
[rawList (Var $ reflm "TTName") (map reflectName ss)]

4
src/Idris/IBC.hs
View File

@ -1420,7 +1420,7 @@ instance Binary Using where
_ -> error "Corrupted binary data for Using"
instance Binary SyntaxInfo where
put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)
put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _)
= do put x1
put x2
put x3
@ -1436,7 +1436,7 @@ instance Binary SyntaxInfo where
x5 <- get
x6 <- get
x7 <- get
return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7 0)
return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0)
instance (Binary t) => Binary (PClause' t) where
put x

2
src/Idris/Prover.hs
View File

@ -78,7 +78,7 @@ prove opt ctxt lit n ty
putIState (i { proof_list = (n, prf) : proofs })
let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]
logLvl 3 (show tree)
(ptm, pty) <- recheckC (fileFC "proof") [] tm
(ptm, pty) <- recheckC (fileFC "proof") id [] tm
logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
"Expected type:" ++ show ty)
case converts ctxt [] ty pty of

2
src/Idris/TypeSearch.hs
View File

@ -46,7 +46,7 @@ searchByType pkgs pterm = do
mapM_ loadPkgIndex pkgs
pterm' <- addUsingConstraints syn emptyFC pterm
pterm'' <- implicit toplevel syn name pterm'
let pterm''' = addImpl i pterm''
let pterm''' = addImpl [] i pterm''
ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'
let names = searchUsing searchPred i ty
let names' = take numLimit names

4
test/quasiquote001/expected
View File

@ -1,5 +1,5 @@
(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN Unit) (TType (UVar -1))))))
--------------
(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 48))) (TType (UVar 50))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 52))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 54)))))
(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 32))) (TType (UVar 34))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 36))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 38)))))
--------------
(App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (TType (UVar 48))) (TType (UVar 48)))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (TType (UVar 48))) (TType (UVar 48))))
(App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (TType (UVar 32))) (TType (UVar 32)))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (TType (UVar 32))) (TType (UVar 32))))

0
test/reg059/expected Normal file
View File

8
test/reg059/reg059.idr Normal file
View File

@ -0,0 +1,8 @@
class Monad m => ContainerMonad (m : Type -> Type) where
Elem : a -> m a -> Type
tagElem : (mx : m a) -> m (x : a ** Elem x mx)
class Monad m => ContainerMonad2 a (m : Type -> Type) where
Elem2 : a -> m a -> Type
tagElem2 : (mx : m a) -> m (x : a ** Elem2 x mx)

3
test/reg059/run Executable file
View File

@ -0,0 +1,3 @@
#!/usr/bin/env bash
idris $@ reg059.idr --check
rm -f *.ibc

2
test/unique001/expected
View File

@ -17,4 +17,4 @@ with
unique001b.idr:16:7:Borrowed name xs must not be used on RHS
unique001c.idr:46:6:Unique name f is used more than once
unique001d.idr:3:7:Borrowed name x must not be used on RHS
unique001e.idr:4:11:Constructor Main.:: has a UniqueType, but the data type does not
unique001e.idr:3:10:Constructor Main.Nil has a UniqueType, but the data type does not