mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 13:36:08 +03:00
[ fix ] respect visibility in forward data declarations
This commit is contained in:
parent
b173267f50
commit
f76c4c4307
@ -467,17 +467,18 @@ processData {vars} eopts nest env fc vis mbtot (MkImpData dfc n_in mty_raw opts
|
||||
-- When looking up, note the data types which were undefined at the
|
||||
-- point of declaration.
|
||||
ndefm <- lookupCtxtExact n (gamma defs)
|
||||
(mw, fullty) <- the (Core (List Name, ClosedTerm)) $ case ndefm of
|
||||
(mw, vis, fullty) <- the (Core (List Name, Visibility, ClosedTerm)) $ case ndefm of
|
||||
Nothing => case mfullty of
|
||||
Nothing => throw (GenericMsg fc "Missing telescope for data definition \{show n_in}")
|
||||
Just fullty => pure ([], fullty)
|
||||
Just fullty => pure ([], vis, fullty)
|
||||
Just ndef =>
|
||||
let vis = max (visibility ndef) vis in
|
||||
case definition ndef of
|
||||
TCon _ _ _ _ _ mw [] _ => case mfullty of
|
||||
Nothing => pure (mw, type ndef)
|
||||
Nothing => pure (mw, vis, type ndef)
|
||||
Just fullty =>
|
||||
do ok <- convert defs [] fullty (type ndef)
|
||||
if ok then pure (mw, fullty)
|
||||
if ok then pure (mw, vis, fullty)
|
||||
else do logTermNF "declare.data" 1 "Previous" [] (type ndef)
|
||||
logTermNF "declare.data" 1 "Now" [] fullty
|
||||
throw (AlreadyDefined fc n)
|
||||
|
@ -269,7 +269,7 @@ idrisTests = MkTestPool "Misc" [] Nothing
|
||||
-- Implicit laziness, lazy evaluation
|
||||
"lazy001", "lazy002",
|
||||
-- Namespace blocks
|
||||
"namespace001", "namespace002", "namespace003",
|
||||
"namespace001", "namespace002", "namespace003", "namespace004",
|
||||
-- Parameters blocks
|
||||
"params001", "params002", "params003",
|
||||
-- Larger programs arising from real usage. Typically things with
|
||||
|
11
tests/idris2/namespace004/Export.idr
Normal file
11
tests/idris2/namespace004/Export.idr
Normal file
@ -0,0 +1,11 @@
|
||||
namespace Core
|
||||
|
||||
public export
|
||||
data D : Type
|
||||
|
||||
|
||||
data D : Type where
|
||||
MkD : D
|
||||
|
||||
d : D
|
||||
d = MkD
|
1
tests/idris2/namespace004/expected
Normal file
1
tests/idris2/namespace004/expected
Normal file
@ -0,0 +1 @@
|
||||
1/1: Building Export (Export.idr)
|
3
tests/idris2/namespace004/run
Normal file
3
tests/idris2/namespace004/run
Normal file
@ -0,0 +1,3 @@
|
||||
rm -rf build
|
||||
|
||||
$1 --no-color --console-width 0 --check Export.idr
|
Loading…
Reference in New Issue
Block a user