816e85b · Idris-dev · git.iko.soy

idris.cabal+6

compare with master

unifiedsplit

@@ -241,6 +241,12 @@ Extra-source-files:

241 test/reg047/run

242 test/reg047/*.idr

243 test/reg047/expected

244+ test/reg048/run

245+ test/reg048/*.idr

246+ test/reg048/expected

247+ test/reg049/run

248+ test/reg049/*.idr

249+ test/reg049/expected

244

250

245 test/basic001/run

251 test/basic001/run

246 test/basic001/*.idr

252 test/basic001/*.idr

src/Idris/ElabDecls.hs+7−4

@@ -395,6 +395,9 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

395 ctxt <- getContext

396 let cty' = normalise ctxt [] cty

397

398+ -- Check that the constructor type is, in fact, a part of the family being defined

399+ tyIs n cty'

400+

398 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

401 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

399 logLvl 5 $ "Inaccessible args: " ++ show inacc

402 logLvl 5 $ "Inaccessible args: " ++ show inacc

400 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

403 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

@@ -407,11 +410,11 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

407 addIBC (IBCOpt n)

410 addIBC (IBCOpt n)

408 return (n, cty')

411 return (n, cty')

409 where

412 where

410− tyIs (Bind n b sc) = tyIs sc

413+ tyIs con (Bind n b sc) = tyIs con sc

411− tyIs t | (P _ n' _, _) <- unApply t

414+ tyIs con t | (P _ n' _, _) <- unApply t

412− = if n' /= tn then tclift $ tfail (At fc (Msg (show n' ++ " is not " ++ show tn)))

415+ = if n' /= tn then tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show n' ++ " is not " ++ show tn))))

413 else return ()

416 else return ()

414− tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))

417+ tyIs con t = tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show t ++ " is not " ++ show tn))))

415

418

416 mkLazy (PPi pl n ty sc)

419 mkLazy (PPi pl n ty sc)

417 = let ty' = if getTyName ty

420 = let ty' = if getTyName ty

test/reg049/expectednew file+2

@@ -0,0 +1,2 @@

1+reg049.idr:2:9:When elaborating constructor Main.Bogus:

2+{__False0} is not Main.Foo

test/reg049/reg049.idrnew file+5

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

1+data Foo : Type where

2+ Bogus : _|_

3+

4+uhOh : _|_

5+uhOh = Bogus

test/reg049/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --nocolour --check $@ reg049.idr

3+rm -f *.ibc