Remove unsafeCoerce from appendIndices and fix tests with GHC 9.0.1#397
Remove unsafeCoerce from appendIndices and fix tests with GHC 9.0.1#397
Conversation
arybczak
force-pushed
the
no-unsafe-coerce-new
branch
3 times, most recently
from
5c1ef7c to
672b751
Compare
arybczak
changed the title
arybczak
force-pushed
the
no-unsafe-coerce-new
branch
4 times, most recently
from
ccee7c8 to
1b41232
Compare
|
Let's see after |
|
I also tried that with the inlineless branch and it was fine 👍 |
|
|
||
| -- | Tagged version of 'Data.Type.Equality.(:~:)' for carrying evidence that two | ||
| -- index lists in a curried form are equal. | ||
| data IxEq i is js where |
| -- | ||
| infixl 9 % | ||
| (%) :: (Is k m, Is l m, m ~ Join k l, ks ~ Append is js) | ||
| (%) :: (Is k m, Is l m, m ~ Join k l, AppendIndices is js, ks ~ Append is js) |
There was a problem hiding this comment.
I think this is generally a good idea, but the only thing that is a slight shame is making the type of % more complicated, with AppendIndices potentially showing up in inferred types. Perhaps it is worth making AppendIndices takes ks as a parameter so that AppendIndices is js ks can imply ks ~ Append is js?
There was a problem hiding this comment.
One could maybe get rid of Append family all together, by having
-appendIndices :: IxEq i (Curry xs (Curry ys i)) (Curry (Append xs ys) i)
+appendIndices :: IxEq i (Curry xs (Curry ys i)) (Curry zs i)... but I guess we cannot as there is no sane way to break functional dependencies in GHCs. Edit i.e. having overlapping FD i.e. the additional incoherent AppendIndicies xs [] xs, if AppendIndicies is js ks | is js -> ks
There was a problem hiding this comment.
One could maybe get rid of Append family all together
I tried that and looks like it works, so I re-added the third parameter and removed dependence on Append.
|
|
||
| -- | If we know the second list is empty, we can pick the first list without | ||
| -- knowing anything about it, hence the instance is marked as INCOHERENT. | ||
| instance {-# INCOHERENT #-} AppendIndices xs '[] where |
There was a problem hiding this comment.
Oh, I thought that FunctionalDependencies would choke on this? Is INCOHERENT making it work somehow?
There was a problem hiding this comment.
It's not INCOHERENT, it's just that the consistency check for fundeps is quite lenient.
|
|
||
| instance AppendIndices xs ys ks => AppendIndices (x ': xs) ys (x ': ks) where | ||
| appendIndices :: forall i. IxEq i (Curry (x ': xs) (Curry ys i)) (Curry (x ': ks) i) | ||
| appendIndices | IxEq <- appendIndices @xs @ys @ks @i = IxEq |
|
It's worth noting that due to Though that shouldn't be a problem in practice since I doubt anyone uses >5 indices in a single pipeline. |
|
re quadratic: wasn't that the case with |
|
Oh, you're right. I thought |
arybczak
force-pushed
the
no-unsafe-coerce-new
branch
from
0cfcb8a to
64c136e
Compare
|
Testing with no INLINE pragmas passed, so I'm merging. |
3 participants
Fixes #396.
This doesn't slow compilation, I tested with a big project.