fbcd643 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Check datatypes are not redefined

We were checking, but only seeing if the type constructor was the same, which is not enough. Fixes #1776.

commitfbcd64372bd9f851ceefb7ea959b9726143ddeb7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 9 Dec 2014, 15:38 (12 years ago) parent58dd2b5

2 files changed+14−9

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+2−2 src/Idris/Elab/Data.hs+12−7

src/Idris/AbsSyntax.hs+2−2

@@ -479,8 +479,8 @@ checkUndefined fc n

479479isUndefined :: FC -> Name -> Idris Bool

480480isUndefined fc n

481481 = do i <- getContext

482− case lookupTy n i of

483− (_:_) -> return False

482+ case lookupTyExact n i of

483+ Just _ -> return False

484484 _ -> return True

485485

486486setContext :: Context -> Idris ()

src/Idris/Elab/Data.hs+12−7

@@ -66,9 +66,10 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

6666 undef <- isUndefined fc n

6767 (cty, _, t, inacc) <- buildType info syn fc [] n t_in

6868 -- if n is defined already, make sure it is just a type declaration

69− -- with the same type we've just elaborated

69+ -- with the same type we've just elaborated, and no constructors

70+ -- yet

7071 i <- getIState

71− checkDefinedAs fc n cty (tt_ctxt i)

72+ checkDefinedAs fc n cty i

7273 -- temporary, to check cons

7374 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)

7475 let cnameinfo = cinfo info (map cname dcons)

@@ -124,14 +125,18 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

124125 [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }

125126 _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }

126127

127− checkDefinedAs fc n t ctxt

128− = case lookupDef n ctxt of

128+ checkDefinedAs fc n t i

129+ = let defined = tclift $ tfail (At fc (AlreadyDefined n))

130+ ctxt = tt_ctxt i in

131+ case lookupDef n ctxt of

129132 [] -> return ()

130133 [TyDecl _ ty] ->

131134 case converts ctxt [] t ty of

132− OK () -> return ()

133− _ -> tclift $ tfail (At fc (AlreadyDefined n))

134− _ -> tclift $ tfail (At fc (AlreadyDefined n))

135+ OK () -> case lookupCtxtExact n (idris_datatypes i) of

136+ Nothing -> return ()

137+ _ -> defined

138+ _ -> defined

139+ _ -> defined

135140 -- parameters are names which are unchanged across the structure,

136141 -- which appear exactly once in the return type of a constructor

137142