Thanks. I'll have to spend some more time thinking through those, but
here's two quick responses.
1) Richard: I thought that because OverlappingInstances was not
specified (in this module or any others), GHC would commit to the
instance. If this behavior you suspect is the case, has there been a
discussion of a flag that would disable it?
2) I think I should leak some more of the details of my actual
situation; they seem important if people want to attempt work arounds
(thanks Gábor).
As you may have guessed, I'm not actually interested in a list of ()s.
My actual class is as follows.
> class NLong (n :: Nat) (ts :: [k])
>
> instance ('[] ~ ps) => NLong Z ps
> instance ((t ': pstail) ~ ps, NLong n pstail) => NLong (S n) ps
I just want to require that the list has n many elements, without
restricting those elements. This is why I'm not using fundeps and type
families — I need to be polymorphic in the elements.
Any alternative ideas given this extra specification details?
-----
Further context: I suspect that my use case for this machinery would
be supplanted if we could promote GADTs (esp. vectors of a fixed
length).
I'll share further technical details about the context if there's
interest. Thanks again!
On Sat, Oct 6, 2012 at 7:30 AM, Gábor Lehel <[email protected]> wrote:
> I made a version using an associated type and that seems to work fine:
>
> https://gist.github.com/3844758
>
> (In fact you probably don't need a class at all and a simple type
> family would be enough.)
>
> On Sat, Oct 6, 2012 at 4:25 AM, Richard Eisenberg <[email protected]> wrote:
>> Hi Nick,
>>
>> Interesting example.
>>
>> I think GHC is right in rejecting your instance, but perhaps not for the
>> reasons you expect.
>>
>> It would be possible to add another instance to NUnits:
>> instance NUnits Z '[()]
>> This would require OverlappingInstances, but because of the possibility of
>> further instances, GHC rightly does not assume that a matching instance is
>> the only possible matching instance. So, without that assumption, there is
>> no reason GHC should unify ts with '[].
>>
>> For similar reasons, GHC does not bring the constraints on an instance into
>> the context when an instance matches. So, even if GHC did select the
>> instance you want, it would not bring ('[] ~ ps) into the context.
>>
>> To me, both of these problems have solutions: introduce a functional
>> dependency on NUnits, n -> ts; and declare the wanted instance to be
>> "instance NUnits Z '[]", without the equality constraint. What's interesting
>> is that doing both of these changes didn't get the instance accepted. This
>> *might* be a bug in GHC, but I'd love another opinion before filing, because
>> I'm really not sure.
>>
>> Another issue at work here is that GHCi, by default, does not enable
>> PolyKinds, even when it has loaded a file with PolyKinds. The effect of this
>> is that printing out polymorphic kinds will see all type variables default
>> to * without :set -XPolyKinds. That may have had a role to play in the
>> commentary in the file, but I'm not sure.
>>
>> Thanks for posting!
>> Richard
>>
>> On Oct 5, 2012, at 5:49 PM, Nicolas Frisby wrote:
>>
>>> GHC 7.6 is rejecting some programs that I think ought to be well-typed.
>>>
>>> Details here https://gist.github.com/3842579
>>>
>>> I find this behavior particularly odd because I can get GHC to deduce
>>> the type equalities in some contexts but not in others. In particular,
>>> it does not deduce them inside of type class instances.
>>>
>>> Is this a known issue? I'll create a Trac ticket if that's appropriate.
>>>
>>> Thanks for your time.
>>>
>>> _______________________________________________
>>> Glasgow-haskell-users mailing list
>>> [email protected]
>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>>
>> _______________________________________________
>> Glasgow-haskell-users mailing list
>> [email protected]
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
>
> --
> Your ship was destroyed in a monadic eruption.
_______________________________________________
Glasgow-haskell-users mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
