f4aaf01 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Guard !! in forgetEnv

This means we get better error messages if there are scoping issues, particularly as caused by 'where' clauses with missing types that can't be inferred. Fixes #1978

commitf4aaf01b348f7aa9d0f93072a16d938614ad199f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 19 Mar 2015, 16:23 (12 years ago) parent15737d9

11 files changed+64−42

compare with master

unifiedsplit

src/Idris/Core/TT.hs+26−10 src/Idris/Elab/Clause.hs+9−9 src/Idris/Elab/Instance.hs+1−1 src/Idris/Elab/Transform.hs+2−2 src/Idris/Elab/Type.hs+3−3 src/Idris/Elab/Utils.hs+16−10 src/Idris/Elab/Value.hs+2−2 src/Idris/ElabTerm.hs+1−1 src/Idris/Prover.hs+1−1 test/quasiquote001/expected+2−2 test/unique001/expected+1−1

src/Idris/Core/TT.hs+26−10

@@ -1170,17 +1170,33 @@ unList tm = case unApply tm of

11701170forget :: TT Name -> Raw

11711171forget tm = forgetEnv [] tm

11721172

1173+safeForget :: TT Name -> Maybe Raw

1174+safeForget tm = safeForgetEnv [] tm

1175+

11731176forgetEnv :: [Name] -> TT Name -> Raw

1174−forgetEnv env (P _ n _) = Var n

1175−forgetEnv env (V i) = Var (env !! i)

1176−forgetEnv env (Bind n b sc) = let n' = uniqueName n env in

1177− RBind n' (fmap (forgetEnv env) b)

1178− (forgetEnv (n':env) sc)

1179−forgetEnv env (App f a) = RApp (forgetEnv env f) (forgetEnv env a)

1180−forgetEnv env (Constant c) = RConstant c

1181−forgetEnv env (TType i) = RType

1182−forgetEnv env (UType u) = RUType u

1183−forgetEnv env Erased = RConstant Forgot

1177+forgetEnv env tm = case safeForgetEnv env tm of

1178+ Just t' -> t'

1179+ Nothing -> error $ "Scope error in " ++ show tm

1180+

1181+

1182+safeForgetEnv :: [Name] -> TT Name -> Maybe Raw

1183+safeForgetEnv env (P _ n _) = Just $ Var n

1184+safeForgetEnv env (V i) | i < length env = Just $ Var (env !! i)

1185+ | otherwise = Nothing

1186+safeForgetEnv env (Bind n b sc)

1187+ = do let n' = uniqueName n env

1188+ b' <- safeForgetEnvB env b

1189+ sc' <- safeForgetEnv (n':env) sc

1190+ Just $ RBind n' b' sc'

1191+ where safeForgetEnvB env (Let t v) = liftM2 Let (safeForgetEnv env t)

1192+ (safeForgetEnv env v)

1193+ safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)

1194+ Just $ fmap (\_ -> ty') b

1195+safeForgetEnv env (App f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)

1196+safeForgetEnv env (Constant c) = Just $ RConstant c

1197+safeForgetEnv env (TType i) = Just RType

1198+safeForgetEnv env (UType u) = Just $ RUType u

1199+safeForgetEnv env Erased = Just $ RConstant Forgot

11841200

11851201-- | Introduce a 'Bind' into the given term for each element of the

11861202-- given list of (name, binder) pairs.

src/Idris/Elab/Clause.hs+9−9

@@ -603,7 +603,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

603603 -- If we're inferring metavariables in the type, don't recheck,

604604 -- because we're only doing this to try to work out those metavariables

605605 (clhs_c, clhsty) <- if not inf

606− then recheckC fc [] lhs_tm

606+ then recheckC fc id [] lhs_tm

607607 else return (lhs_tm, lhs_ty)

608608 let clhs = normalise ctxt [] clhs_c

609609 let borrowed = borrowedNames [] clhs

@@ -681,7 +681,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

681681 logLvl 4 $ "---> " ++ show rhs'

682682 when (not (null defer)) $ iLOG $ "DEFERRED " ++

683683 show (map (\ (n, (_,_,t)) -> (n, t)) defer)

684− def' <- checkDef fc defer

684+ def' <- checkDef fc (Elaborating "deferred type of ") defer

685685 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

686686 addDeferred def''

687687 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

700700 logLvl 6 $ " ==> " ++ show (forget rhs')

701701

702702 (crhs, crhsty) <- if not inf

703− then recheckC_borrowing True borrowed fc [] rhs'

703+ then recheckC_borrowing True borrowed fc id [] rhs'

704704 else return (rhs', clhsty)

705705 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

706706 ctxt <- getContext

@@ -828,7 +828,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

828828 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

829829 let static_names = getStaticNames i lhs_tm

830830 logLvl 5 (show lhs_tm ++ "\n" ++ show static_names)

831− (clhs, clhsty) <- recheckC fc [] lhs_tm

831+ (clhs, clhsty) <- recheckC fc id [] lhs_tm

832832 logLvl 5 ("Checked " ++ show clhs)

833833 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

834834 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)

847847 return (tt, d, is, ctxt', newDecls))

848848 setContext ctxt'

849849 processTacticDecls newDecls

850− def' <- checkDef fc defer

850+ def' <- checkDef fc iderr defer

851851 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

852852 addDeferred def''

853853 mapM_ (elabCaseBlock info opts) is

854854 logLvl 5 ("Checked wval " ++ show wval')

855− (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')

855+ (cwval, cwvalty) <- recheckC fc id [] (getInferTerm wval')

856856 let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)

857857 let cwvalN = explicitNames (normalise ctxt [] cwval)

858858 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)

907907 addIBC (IBCImp wname)

908908 addIBC (IBCStatic wname)

909909

910− def' <- checkDef fc [(wname, (-1, Nothing, wtype))]

910+ def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype))]

911911 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

912912 addDeferred def''

913913

@@ -943,12 +943,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

943943 setContext ctxt'

944944 processTacticDecls newDecls

945945

946− def' <- checkDef fc defer

946+ def' <- checkDef fc iderr defer

947947 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

948948 addDeferred def''

949949 mapM_ (elabCaseBlock info opts) is

950950 logLvl 5 ("Checked RHS " ++ show rhs')

951− (crhs, crhsty) <- recheckC fc [] rhs'

951+ (crhs, crhsty) <- recheckC fc id [] rhs'

952952 return $ (Right (clhs, crhs), lhs)

953953 where

954954 getImps (Bind n (Pi _ _ _) t) = pexp Placeholder : getImps t

src/Idris/Elab/Instance.hs+1−1

@@ -175,7 +175,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

175175 setContext ctxt'

176176 processTacticDecls newDecls

177177 ctxt <- getContext

178− (cty, _) <- recheckC fc [] tyT

178+ (cty, _) <- recheckC fc id [] tyT

179179 let nty = normalise ctxt [] cty

180180 return $ any (isJust . findOverlapping i (class_determiners ci) (delab i nty)) (class_instances ci)

181181

src/Idris/Elab/Transform.hs+2−2

@@ -63,7 +63,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

6363 let lhs_ty = getInferType lhs'

6464 let newargs = pvars i lhs_tm

6565

66− (clhs_tm_in, clhs_ty) <- recheckC fc [] lhs_tm

66+ (clhs_tm_in, clhs_ty) <- recheckC fc id [] lhs_tm

6767 let clhs_tm = renamepats pnames clhs_tm_in

6868 logLvl 3 ("Transform LHS " ++ show clhs_tm)

6969

@@ -80,7 +80,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

8080 setContext ctxt'

8181 processTacticDecls newDecls

8282

83− (crhs_tm_in, crhs_ty) <- recheckC fc [] rhs'

83+ (crhs_tm_in, crhs_ty) <- recheckC fc id [] rhs'

8484 let crhs_tm = renamepats pnames crhs_tm_in

8585 logLvl 3 ("Transform RHS " ++ show crhs_tm)

8686

src/Idris/Elab/Type.hs+3−3

@@ -75,7 +75,7 @@ buildType info syn fc opts n ty' = do

7575

7676 logLvl 3 $ show ty ++ "\nElaborated: " ++ show tyT'

7777

78− ds <- checkAddDef True False fc defer

78+ ds <- checkAddDef True False fc iderr defer

7979 -- if the type is not complete, note that we'll need to infer

8080 -- things later (for solving metavariables)

8181 when (not (null ds)) $ addTyInferred n

@@ -85,7 +85,7 @@ buildType info syn fc opts n ty' = do

8585 logLvl 5 $ "Rechecking"

8686 logLvl 6 $ show tyT

8787 logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT

88− (cty, ckind) <- recheckC fc [] tyT

88+ (cty, ckind) <- recheckC fc id [] tyT

8989

9090 -- record the implicit and inaccessible arguments

9191 i <- getIState

@@ -154,7 +154,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

154154 -- Productivity checking now via checking for guarded 'Delay'

155155 let opts' = opts -- if corec then (Coinductive : opts) else opts

156156 let usety = if norm then nty' else nty

157− ds <- checkDef fc [(n, (-1, Nothing, usety))]

157+ ds <- checkDef fc iderr [(n, (-1, Nothing, usety))]

158158 addIBC (IBCDef n)

159159 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

160160 addDeferred ds'

src/Idris/Elab/Utils.hs+16−10

@@ -24,30 +24,36 @@ import qualified Data.Map as Map

2424

2525recheckC = recheckC_borrowing False []

2626

27−recheckC_borrowing uniq_check bs fc env t

27+recheckC_borrowing uniq_check bs fc mkerr env t

2828 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

2929 ctxt <- getContext

30− (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env (forget t) t of

31− Error e -> tfail (At fc e)

30+ t' <- case safeForget t of

31+ Just ft -> return ft

32+ Nothing -> tclift $ tfail $ mkerr (At fc (IncompleteTerm t))

33+ (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env t' t of

34+ Error e -> tfail (At fc (mkerr e))

3235 OK x -> return x

3336 logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs

3437 addConstraints fc cs

3538 return (tm, ty)

3639

37−checkDef :: FC -> [(Name, (Int, Maybe Name, Type))]

40+iderr :: Name -> Err -> Err

41+iderr _ e = e

42+

43+checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))]

3844 -> Idris [(Name, (Int, Maybe Name, Type))]

39−checkDef fc ns = checkAddDef False True fc ns

45+checkDef fc mkerr ns = checkAddDef False True fc mkerr ns

4046

41−checkAddDef :: Bool -> Bool -> FC

47+checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)

4248 -> [(Name, (Int, Maybe Name, Type))]

4349 -> Idris [(Name, (Int, Maybe Name, Type))]

44−checkAddDef add toplvl fc [] = return []

45−checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

50+checkAddDef add toplvl fc mkerr [] = return []

51+checkAddDef add toplvl fc mkerr ((n, (i, top, t)) : ns)

4652 = do ctxt <- getContext

47− (t', _) <- recheckC fc [] t

53+ (t', _) <- recheckC fc (mkerr n) [] t

4854 when add $ do addDeferred [(n, (i, top, t, toplvl))]

4955 addIBC (IBCDef n)

50− ns' <- checkAddDef add toplvl fc ns

56+ ns' <- checkAddDef add toplvl fc mkerr ns

5157 return ((n, (i, top, t')) : ns')

5258

5359-- | Get the list of (index, name) of inaccessible arguments from an elaborated

src/Idris/Elab/Value.hs+2−2

@@ -73,13 +73,13 @@ elabValBind info aspat norm tm_in

7373

7474 let vtm = orderPats (getInferTerm tm')

7575

76− def' <- checkDef (fileFC "(input)") defer

76+ def' <- checkDef (fileFC "(input)") iderr defer

7777 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

7878 addDeferred def''

7979 mapM_ (elabCaseBlock info []) is

8080

8181 logLvl 3 ("Value: " ++ show vtm)

82− (vtm_in, vty) <- recheckC (fileFC "(input)") [] vtm

82+ (vtm_in, vty) <- recheckC (fileFC "(input)") id [] vtm

8383

8484 let vtm = if norm then normalise (tt_ctxt i) [] vtm_in

8585 else vtm_in

src/Idris/ElabTerm.hs+1−1

@@ -57,7 +57,7 @@ processTacticDecls info =

5757 updateIState $ \i -> i { idris_implicits =

5858 addDef n impls (idris_implicits i) }

5959 addIBC (IBCImp n)

60− ds <- checkDef fc [(n, (-1, Nothing, ty))]

60+ ds <- checkDef fc iderr [(n, (-1, Nothing, ty))]

6161 addIBC (IBCDef n)

6262 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

6363 addDeferred ds'

src/Idris/Prover.hs+1−1

@@ -78,7 +78,7 @@ prove opt ctxt lit n ty

7878 putIState (i { proof_list = (n, prf) : proofs })

7979 let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

8080 logLvl 3 (show tree)

81− (ptm, pty) <- recheckC (fileFC "proof") [] tm

81+ (ptm, pty) <- recheckC (fileFC "proof") id [] tm

8282 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++

8383 "Expected type:" ++ show ty)

8484 case converts ctxt [] ty pty of

test/quasiquote001/expected+2−2

@@ -1,5 +1,5 @@

11(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))))))

22--------------

3−(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)))))

3+(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)))))

44--------------

5−(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))))

5+(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))))

test/unique001/expected+1−1

@@ -17,4 +17,4 @@ with

1717unique001b.idr:16:7:Borrowed name xs must not be used on RHS

1818unique001c.idr:46:6:Unique name f is used more than once

1919unique001d.idr:3:7:Borrowed name x must not be used on RHS

20−unique001e.idr:4:11:Constructor Main.:: has a UniqueType, but the data type does not

20+unique001e.idr:3:10:Constructor Main.Nil has a UniqueType, but the data type does not