f4aaf01 · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

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

1170forget :: TT Name -> Raw

1171forget tm = forgetEnv [] tm

1172

1173+safeForget :: TT Name -> Maybe Raw

1174+safeForget tm = safeForgetEnv [] tm

1175+

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

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

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

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

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

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

1185+ | otherwise = Nothing

1186+safeForgetEnv env (Bind n b sc)

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

1187+ = do let n' = uniqueName n env

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

1188+ b' <- safeForgetEnvB env b

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

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

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

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)

1180−forgetEnv env (Constant c) = RConstant c

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

1181−forgetEnv env (TType i) = RType

1197+safeForgetEnv env (TType i) = Just RType

1182−forgetEnv env (UType u) = RUType u

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

1183−forgetEnv env Erased = RConstant Forgot

1199+safeForgetEnv env Erased = Just $ RConstant Forgot

1184

1200

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

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

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

1202-- 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

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

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

605 (clhs_c, clhsty) <- if not inf

606− then recheckC fc [] lhs_tm

606+ then recheckC fc id [] lhs_tm

607 else return (lhs_tm, lhs_ty)

608 let clhs = normalise ctxt [] clhs_c

609 let borrowed = borrowedNames [] clhs

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

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

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

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

684− def' <- checkDef fc defer

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

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

686 addDeferred def''

687 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

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

701

702 (crhs, crhsty) <- if not inf

703− then recheckC_borrowing True borrowed fc [] rhs'

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

704 else return (rhs', clhsty)

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

706 ctxt <- getContext

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

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

829 let static_names = getStaticNames i lhs_tm

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

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

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

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

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

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

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

848 setContext ctxt'

849 processTacticDecls newDecls

850− def' <- checkDef fc defer

850+ def' <- checkDef fc iderr defer

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

852 addDeferred def''

853 mapM_ (elabCaseBlock info opts) is

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

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

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

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

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

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

907 addIBC (IBCImp wname)

908 addIBC (IBCStatic wname)

909

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

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

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

912 addDeferred def''

913

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

943 setContext ctxt'

944 processTacticDecls newDecls

945

946− def' <- checkDef fc defer

946+ def' <- checkDef fc iderr defer

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

948 addDeferred def''

949 mapM_ (elabCaseBlock info opts) is

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

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

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

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

953 where

954 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

175 setContext ctxt'

176 processTacticDecls newDecls

177 ctxt <- getContext

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

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

179 let nty = normalise ctxt [] cty

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

181

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

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

63 let lhs_ty = getInferType lhs'

64 let newargs = pvars i lhs_tm

65

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

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

67 let clhs_tm = renamepats pnames clhs_tm_in

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

69

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

80 setContext ctxt'

81 processTacticDecls newDecls

82

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

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

84 let crhs_tm = renamepats pnames crhs_tm_in

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

86

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

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

75

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

77

78− ds <- checkAddDef True False fc defer

78+ ds <- checkAddDef True False fc iderr defer

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

80 -- things later (for solving metavariables)

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

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

85 logLvl 5 $ "Rechecking"

86 logLvl 6 $ show tyT

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

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

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

89

90 -- record the implicit and inaccessible arguments

91 i <- getIState

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

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

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

156 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))]

158 addIBC (IBCDef n)

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

160 addDeferred ds'

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

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

24

25recheckC = recheckC_borrowing False []

26

27−recheckC_borrowing uniq_check bs fc env t

27+recheckC_borrowing uniq_check bs fc mkerr env t

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

29 ctxt <- getContext

30+ t' <- case safeForget t of

31+ Just ft -> return ft

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

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

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

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

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

32 OK x -> return x

35 OK x -> return x

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

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

34 addConstraints fc cs

37 addConstraints fc cs

35 return (tm, ty)

38 return (tm, ty)

36

39

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

41+iderr _ e = e

42+

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

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

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

44 -> 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

40

46

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

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

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

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

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

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

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

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

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

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

46 = do ctxt <- getContext

52 = do ctxt <- getContext

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

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

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

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

49 addIBC (IBCDef n)

55 addIBC (IBCDef n)

50− ns' <- checkAddDef add toplvl fc ns

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

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

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

52

58

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

59-- | 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

73

74 let vtm = orderPats (getInferTerm tm')

75

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

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

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

78 addDeferred def''

79 mapM_ (elabCaseBlock info []) is

80

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

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

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

83

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

85 else vtm_in

src/Idris/ElabTerm.hs+1−1

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

57 updateIState $ \i -> i { idris_implicits =

58 addDef n impls (idris_implicits i) }

59 addIBC (IBCImp n)

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

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

61 addIBC (IBCDef n)

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

63 addDeferred ds'

src/Idris/Prover.hs+1−1

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

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

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

80 logLvl 3 (show tree)

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

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

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

83 "Expected type:" ++ show ty)

84 case converts ctxt [] ty pty of

test/quasiquote001/expected+2−2

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

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

2--------------

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

4--------------

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

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

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

19unique001d.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