git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3936 from mandubian/fix/master/1211

Fixes #1211 : default impl in interfaces through parent constraints recursively

commite03ff3d34237ae2baf51e553ea715725897556e6 authorEdwin Brady <edwin.brady@gmail.com> dateSat 2 Sep 2017, 19:11 (9 years ago) parent4251ad8532ef6c
7 files changed+40−4
compare with master
unifiedsplit
src/Idris/Core/CaseTree.hs+1 src/Idris/Elab/Interface.hs+11−2 src/Util/DynamicLinker.hs+1−1 test/TestData.hs+2−1 test/interfaces008/expected+2 test/interfaces008/interfaces008.idr+20 test/interfaces008/run+3
src/Idris/Core/CaseTree.hs+1
@@ -18,6 +18,7 @@ allows casing on arbitrary terms, here we choose to maintain the distinction
1818in order to allow for better optimisation opportunities.
1919
2020-}
21+
2122{-# LANGUAGE DeriveFunctor, DeriveGeneric, FlexibleContexts, FlexibleInstances,
2223 PatternGuards, TypeSynonymInstances #-}
2324
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
src/Util/DynamicLinker.hs+1−1
@@ -14,7 +14,7 @@ module Util.DynamicLinker ( ForeignFun(..)
1414
1515#ifdef IDRIS_FFI
1616import Foreign.LibFFI
17−import Foreign.Ptr (FunPtr, Ptr(), castPtrToFunPtr, nullFunPtr, nullPtr)
17+import Foreign.Ptr (FunPtr, Ptr, castPtrToFunPtr, nullFunPtr, nullPtr)
1818import System.Directory
1919#ifndef mingw32_HOST_OS
2020import Control.Exception (IOException, throwIO, try)
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