On Mon, Apr 23, 2018 at 04:54:36PM +0200, Marc Busqué wrote:
On Mon, 23 Apr 2018, Tom Ellis wrote:
I had an error in what I said and also it was imprecise. It's `Res (Cols s a)` which is `a`, but only in the cases where you're actually going to use it, and the compiler cannot take that into account when solving the constraint. Anyway, as Li-yao Xia points out in a sibling message, the type variable `s` in not constrained and therefore it seems impossible to solve.
I have pushed the repo to Github:
Thanks for that Marc, it's very helpful. I extracted the parts that are relevant to the problem and created a version that doesn't depend on Selda: https://gist.github.com/tomjaguarpaw/f4db46671e2f39b790a25b8907dc53a3 I think I now understand what the situation is. Interestingly your code works on 8.0 but not 7.10. Contrary to my earlier presumptions, the compiler *is* able to give a type to `list` because `Cols` is a closed type family. I suppose it can determine that `Cols s a` does not actually depend on `s` so giving list the type (Result (Cols s a), Columns (Cols s a)) => Table a -> Res (Cols s a) is fine. The type of `s` will never be needed. When `list` is applied to `categories` then `a` is fixed and `Res (Cols s a)` is fixed, regardless of what `s` is. Subtly changing the definition of Cols will break things. For example, if you add the clause Cols () a = Col Int a then you won't be able to define `list` any more, even though `Res (Cols s a)` is still just `a` because the `Columns (Cols s a)` instance might then depend on what `s` is. On the other hand, I do not yet understand why you cannot provide an explicit signature for `list`. I suspect this is some hairy compiler bug. Either it should be possible to give `list` its inferred type or it should be forbidden. It's probably worth filing an issue about this on GHC Trac. I would be interested to hear Li-yao's thoughts on the matter. Incidentally, this is why I try to avoid type families as much as possible. When they go wrong it's very hard to understand why, and indeed when they go right it's also very hard to understand why. Tom