seemingly inconsistent behavior for "kind-indexed" type constraints in GHC 7.6
illissius at gmail.com
Sat Oct 6 19:46:05 CEST 2012
On Sat, Oct 6, 2012 at 7:17 PM, Nicolas Frisby <nicolas.frisby at gmail.com> 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
> Further context: I suspect that my use case for this machinery would
> be supplanted if we could promote GADTs (esp. vectors of a fixed
> 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 <illissius at gmail.com> wrote:
>> I made a version using an associated type and that seems to work fine:
>> (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 <eir at cis.upenn.edu> 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!
>>> 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
>>>> Glasgow-haskell-users at haskell.org
>>> Glasgow-haskell-users mailing list
>>> Glasgow-haskell-users at haskell.org
>> Your ship was destroyed in a monadic eruption.
Your ship was destroyed in a monadic eruption.
More information about the Glasgow-haskell-users