416251f · Idris-dev · git.iko.soy

src/Idris/Elab/Interface.hs+11−2

compare with master

unifiedsplit

@@ -270,11 +270,20 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn

270 = do when (not $ null cs) . tclift

271 $ tfail (At fc (Msg "Default super interface implementations can't have constraints."))

272 i <- getIState

273− let t = PApp fc (PRef fc [] n) (map pexp ps)

273+ let isConstrained = any (checkConstrained i n (map pexp ps)) (map snd constraints)

274− let isConstrained = any (== t) (map snd constraints)

275 when (not isConstrained) . tclift

274 when (not isConstrained) . tclift

276 $ tfail (At fc (Msg "Default implementations must be for a super interface constraint on the containing interface."))

275 $ tfail (At fc (Msg "Default implementations must be for a super interface constraint on the containing interface."))

277 return ()

276 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))

278

287

279 checkConstraintName :: [Name] -> Name -> Idris ()

288 checkConstraintName :: [Name] -> Name -> Idris ()

280 checkConstraintName bound cname

289 checkConstraintName bound cname

test/TestData.hs+2−1

@@ -165,7 +165,8 @@ testFamiliesData = [

165 ( 4, ANY ),

166-- ( 5, ANY ),

167 ( 6, ANY ),

168− ( 7, ANY )]),

168+ ( 7, ANY ),

169+ ( 8, ANY )]),

169 ("interpret", "Interpret",

170 ("interpret", "Interpret",

170 [ ( 1, ANY ),

171 [ ( 1, ANY ),

171 ( 2, ANY )]),

172 ( 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