Merge pull request #4185 from ahmadsalim/feature/named-non-injective-impls
Ensure only injectivity if not named
commitac06bdfd046f0586cffc4373671a156cfddeccef
authorAhmad Salim Al-Sibahi <asal@itu.dk>
dateWed 8 Nov 2017, 22:12 (9 years ago)
parent683be9b249ff98
CHANGELOG.md+9
@@ -14,6 +14,15 @@
1414 other operators, e.g. ``infixr 8 `cons` ``. Backticked operators with
1515 undeclared fixity are treated as non-associative with precedence lower
1616 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}`.
1726
1827## Library Updates
1928
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
7777 _ -> addImplementation intImpl False n iname
7878
7979 ist <- getIState
80− checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))
80+ when (isNothing expn) $
81+ checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))
8182
8283 when (what /= ETypes && (not (null ds && not emptyinterface))) $ do
8384 -- 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