On Sat, Oct 6, 2012 at 7:17 PM, Nicolas Frisby <[email protected]> wrote:
> 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?
What do you use NLong for? I.e. where and how are you taking advantage
of the knowledge that the list is N long?
You could do
type family Length (l :: '[k]) :: Nat
type instance Length '[] = Z
type instance Length (x ': xs) = S (Length xs)
class (Length l ~ n) => NLong n l
instance (Length l ~ n) => NLong n l
and though I didn't try it that would presumably in fact restrict the
list to be that long, but I'm not sure you could use it to prove
things to the typechecker (though I also don't know what you want to
prove).
>
> -----
>
> 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.
--
Your ship was destroyed in a monadic eruption.
_______________________________________________
Glasgow-haskell-users mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
