mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-11 16:05:51 +03:00
Bugfix #269
Make desugaring/elaboration of interfaces, interface implementations, records, and parameter blocks take into account the pragma `%unbound_implicits off`. Main changes: (a) Execute the pragma also during desugaring (b) Check whether `isUnboundImplicits` is on at each desugaring step Alternatives I didn't take: (1) Changing `findBindableNames` to effectfully check the flag. Rationale: Apart from turning a pure function into an effectful one, this would mean repeatedly calling `findBindableNames`, only to do nothing once the flag is read. (2) Adding another function that takes multiple places (list of terms) that might contain bindable names, and before dispatching `findBindableNames` on each term, checking the flag. Rationale: I didn't want to add another abstraction. (weak rationale) @edwinb @gallais : if you prefer (2), I can do that.
This commit is contained in:
parent
59503712f3
commit
fbf82eaf0b
@ -630,9 +630,12 @@ mutual
|
||||
params' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
|
||||
pure (fst ntm, tm')) params
|
||||
-- Look for implicitly bindable names in the parameters
|
||||
let pnames = concatMap (findBindableNames True
|
||||
pnames <- if !isUnboundImplicits
|
||||
then pure $
|
||||
concatMap (findBindableNames True
|
||||
(ps ++ map fst params) [])
|
||||
(map snd params')
|
||||
else pure []
|
||||
let paramsb = map (\ (n, tm) => (n, doBind pnames tm)) params'
|
||||
pure [IParameters fc paramsb (concat pds')]
|
||||
desugarDecl ps (PUsing fc uimpls uds)
|
||||
@ -658,12 +661,15 @@ mutual
|
||||
pure (fst ntm, tm')) params
|
||||
-- Look for bindable names in all the constraints and parameters
|
||||
let mnames = map dropNS (definedIn body)
|
||||
let bnames = concatMap (findBindableNames True
|
||||
bnames <- if !isUnboundImplicits
|
||||
then pure $
|
||||
concatMap (findBindableNames True
|
||||
(ps ++ mnames ++ map fst params) [])
|
||||
(map snd cons') ++
|
||||
concatMap (findBindableNames True
|
||||
(ps ++ mnames ++ map fst params) [])
|
||||
(map snd params')
|
||||
else pure []
|
||||
let paramsb = map (\ (n, tm) => (n, doBind bnames tm)) params'
|
||||
let consb = map (\ (n, tm) => (n, doBind bnames tm)) cons'
|
||||
|
||||
@ -692,8 +698,11 @@ mutual
|
||||
pure (fst ntm, tm')) cons
|
||||
params' <- traverse (desugar AnyExpr ps) params
|
||||
-- Look for bindable names in all the constraints and parameters
|
||||
let bnames = concatMap (findBindableNames True ps []) (map snd cons') ++
|
||||
bnames <- if !isUnboundImplicits
|
||||
then pure $
|
||||
concatMap (findBindableNames True ps []) (map snd cons') ++
|
||||
concatMap (findBindableNames True ps []) params'
|
||||
else pure []
|
||||
let paramsb = map (doBind bnames) params'
|
||||
let isb = map (\ (n, r, tm) => (n, r, doBind bnames tm)) is'
|
||||
let consb = map (\ (n, tm) => (n, doBind bnames tm)) cons'
|
||||
@ -710,9 +719,13 @@ mutual
|
||||
pure (fst ntm, tm')) params
|
||||
let fnames = map fname fields
|
||||
-- Look for bindable names in the parameters
|
||||
let bnames = concatMap (findBindableNames True
|
||||
|
||||
bnames <- if !isUnboundImplicits
|
||||
then pure $
|
||||
concatMap (findBindableNames True
|
||||
(ps ++ fnames ++ map fst params) [])
|
||||
(map snd params')
|
||||
else pure []
|
||||
fields' <- traverse (desugarField (ps ++ fnames ++ map fst params))
|
||||
fields
|
||||
let paramsb = map (\ (n, tm) => (n, doBind bnames tm)) params'
|
||||
@ -757,7 +770,9 @@ mutual
|
||||
Hide n => pure [IPragma (\c, nest, env => hide fc n)]
|
||||
Logging i => pure [ILog i]
|
||||
LazyOn a => pure [IPragma (\c, nest, env => lazyActive a)]
|
||||
UnboundImplicits a => pure [IPragma (\c, nest, env => setUnboundImplicits a)]
|
||||
UnboundImplicits a => do
|
||||
setUnboundImplicits a
|
||||
pure [IPragma (\c, nest, env => setUnboundImplicits a)]
|
||||
AmbigDepth n => pure [IPragma (\c, nest, env => setAmbigLimit n)]
|
||||
PairNames ty f s => pure [IPragma (\c, nest, env => setPair fc ty f s)]
|
||||
RewriteName eq rw => pure [IPragma (\c, nest, env => setRewrite fc eq rw)]
|
||||
|
@ -141,7 +141,10 @@ elabImplementation {vars} fc vis pass env nest is cons iname ps impln nusing mbo
|
||||
|
||||
let initTy = bindImpls fc is $ bindConstraints fc AutoImplicit cons
|
||||
(apply (IVar fc iname) ps)
|
||||
let paramBinds = findBindableNames True vars [] initTy
|
||||
paramBinds <- if !isUnboundImplicits
|
||||
then pure $
|
||||
findBindableNames True vars [] initTy
|
||||
else pure []
|
||||
let impTy = doBind paramBinds initTy
|
||||
|
||||
let impTyDecl = IClaim fc RigW vis opts (MkImpTy fc impName impTy)
|
||||
|
@ -77,7 +77,7 @@ idrisTests
|
||||
"record001", "record002",
|
||||
-- Miscellaneous regressions
|
||||
"reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
|
||||
"reg008", "reg009", "reg010", "reg011", "reg012",
|
||||
"reg008", "reg009", "reg010", "reg011", "reg012", "reg013",
|
||||
-- Totality checking
|
||||
"total001", "total002", "total003", "total004", "total005",
|
||||
"total006",
|
||||
|
17
tests/idris2/reg013/UnboundImplicits.idr
Normal file
17
tests/idris2/reg013/UnboundImplicits.idr
Normal file
@ -0,0 +1,17 @@
|
||||
||| Tests for issue #269
|
||||
import Data.Vect
|
||||
|
||||
%unbound_implicits off
|
||||
|
||||
record Foo (x : Vect n Nat) where
|
||||
constructor MkFoo
|
||||
|
||||
parameters (Foo : Vect n Nat)
|
||||
bar : Nat
|
||||
bar = 0
|
||||
|
||||
|
||||
interface Foo (a : Vect n Nat) where
|
||||
baz : Nat
|
||||
|
||||
implementation Functor (Vect n) where
|
8
tests/idris2/reg013/expected
Normal file
8
tests/idris2/reg013/expected
Normal file
@ -0,0 +1,8 @@
|
||||
1/1: Building UnboundImplicits (UnboundImplicits.idr)
|
||||
UnboundImplicits.idr:6:22--6:24:While processing constructor Foo at UnboundImplicits.idr:6:1--9:1:
|
||||
Undefined name n
|
||||
UnboundImplicits.idr:9:24--9:26:Undefined name n
|
||||
UnboundImplicits.idr:14:25--14:27:While processing constructor Foo at UnboundImplicits.idr:14:1--17:1:
|
||||
Undefined name n
|
||||
UnboundImplicits.idr:17:30--17:31:While processing type of Functor implementation at UnboundImplicits.idr:17:1--18:1 at UnboundImplicits.idr:17:1--18:1:
|
||||
Undefined name n
|
3
tests/idris2/reg013/run
Executable file
3
tests/idris2/reg013/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 UnboundImplicits.idr --check
|
||||
|
||||
rm -rf build
|
Loading…
Reference in New Issue
Block a user