git.iko.soy/Idris-dev
on master help sign in
Fixes #1211 : checking default impl in interfaces through parent constraints recursively

Updated checkDefaultSuperInterfaceImplementation to check default implementations nested in interfaces with respect to constraints of containing interface and if not found, recursively search through constraints of parent interfaces.

commit416251f32374914fb12e2bcac8607317b037fb71 authormandubian <pascal@projectseptember.com> dateSat 22 Jul 2017, 22:40 (9 years ago) parente32f5cd
5 files changed+38−3
compare with master
unifiedsplit
src/Idris/Elab/Interface.hs+11−2 test/TestData.hs+2−1 test/interfaces008/expected+2 test/interfaces008/interfaces008.idr+20 test/interfaces008/run+3
src/Idris/Elab/Interface.hs+11−2
@@ -270,11 +270,20 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn
270270 = do when (not $ null cs) . tclift
271271 $ tfail (At fc (Msg "Default super interface implementations can't have constraints."))
272272 i <- getIState
273− let t = PApp fc (PRef fc [] n) (map pexp ps)
274− let isConstrained = any (== t) (map snd constraints)
273+ let isConstrained = any (checkConstrained i n (map pexp ps)) (map snd constraints)
275274 when (not isConstrained) . tclift
276275 $ tfail (At fc (Msg "Default implementations must be for a super interface constraint on the containing interface."))
277276 return ()
277+ where
278+ -- First, Check that interface "constraint" has same name & args as default implementation name & args (not checking FC)
279+ -- If not the case, recursively lookup in context for parent interface & recheck the same with parent constraints
280+ checkConstrained i n args constraint =
281+ if (n == cn && args == cargs)
282+ then True
283+ else any (id) (map (checkConstrained i n args) parentConstraints)
284+ where
285+ PApp _ (PRef _ _ cn) cargs = constraint
286+ parentConstraints = concatMap interface_constraints (lookupCtxt cn (idris_interfaces i))
278287
279288 checkConstraintName :: [Name] -> Name -> Idris ()
280289 checkConstraintName bound cname
test/TestData.hs+2−1
@@ -165,7 +165,8 @@ testFamiliesData = [
165165 ( 4, ANY ),
166166-- ( 5, ANY ),
167167 ( 6, ANY ),
168− ( 7, ANY )]),
168+ ( 7, ANY ),
169+ ( 8, ANY )]),
169170 ("interpret", "Interpret",
170171 [ ( 1, ANY ),
171172 ( 2, ANY )]),
test/interfaces008/expectednew file+2
@@ -0,0 +1,2 @@
1+interfaces008.idr:20:18:
2+Default implementations must be for a super interface constraint on the containing interface.
test/interfaces008/interfaces008.idrnew file+20
@@ -0,0 +1,20 @@
1+interface Foo a where
2+
3+interface Foo2 a where
4+
5+interface Foo a => Bar a where
6+
7+interface Foo a => Bar2 a where
8+ implementation Foo a where
9+
10+-- Foo is found in parent
11+interface Bar a => Bar3 a where
12+ implementation Foo a where
13+
14+-- not necessary but should compile
15+interface (Foo a, Bar a) => Bar4 a where
16+ implementation Foo a where
17+
18+-- should fail to compile (Foo2 isn't found in parent interfaces)
19+interface Foo a => Bar5 a where
20+ implementation Foo2 a where
test/interfaces008/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces008.idr --noprelude --check
3+rm -f interfaces008 *.ibc