git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4185 from ahmadsalim/feature/named-non-injective-impls
ac06bdfAhmad Salim Al-Sibahi
CHANGELOG.md+9
compare with master
unifiedsplit
@@ -14,6 +14,15 @@
14 other operators, e.g. ``infixr 8 `cons` ``. Backticked operators with
14 other operators, e.g. ``infixr 8 `cons` ``. Backticked operators with
15 undeclared fixity are treated as non-associative with precedence lower
15 undeclared fixity are treated as non-associative with precedence lower
16 than all declared operators.
16 than all declared operators.
17++ Allow non-injective implementations if explicitly named, e.g.,
18+ ```idris
19+ LTB : Nat -> Type
20+ LTB b = DPair Nat (\ n => LT n b)
21+
22+ implementation [uninhabltb] Uninhabited (LTB Z) where
23+ uninhabited (MkDPair n prf) = absurd prf
24+ ```
25+ It is possible to use `using implementation uninhabltb` to add the implementation to the automated resolution, but if it fails to find the instance due to non-injectivity, one must pass it explicitly to target function, i.e. `absurd @{uninhabltb}`.
17
26
18## Library Updates
27## Library Updates
19
28
src/Idris/Elab/Implementation.hs+2−1
@@ -77,7 +77,8 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
77 _ -> addImplementation intImpl False n iname
77 _ -> addImplementation intImpl False n iname
78
78
79 ist <- getIState
79 ist <- getIState
80+ when (isNothing expn) $
80− checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))
81+ checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))
81
82
82 when (what /= ETypes && (not (null ds && not emptyinterface))) $ do
83 when (what /= ETypes && (not (null ds && not emptyinterface))) $ do
83 -- Add the parent implementation names to the privileged set
84 -- Add the parent implementation names to the privileged set
test/interfaces009/expectednew file

No changes to the content.

test/interfaces009/interfaces009.idrnew file+24
@@ -0,0 +1,24 @@
1+module Test
2+
3+LTE : (x, y : Double) -> Type
4+
5+NonNegDouble : Type
6+NonNegDouble = Subset Double (\ x => 0.0 `LTE` x)
7+
8+plus : (x, y : NonNegDouble) -> NonNegDouble
9+
10+mult : (x, y : NonNegDouble) -> NonNegDouble
11+
12+fromIntegerNN : Integer -> NonNegDouble
13+
14+implementation [numnnd] Num NonNegDouble where
15+ (+) = plus
16+ (*) = mult
17+ fromInteger = fromIntegerNN
18+
19+using implementation numnnd
20+ x : NonNegDouble
21+ y : NonNegDouble
22+ z : NonNegDouble
23+ z = x + y
24+
test/interfaces009/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces009.idr --noprelude --check
3+rm -f interfaces009 *.ibc