Repeated variables in type family instances

[Dominique Devriese]

Richard,

I'm interested by your argument at the bottom of the wiki page about
the alternative (non-)solution of disallowing non-linear patterns
altogether.  I'll quote it for reference:

  One way we (Simon, Dimitrios, and Richard) considered proceeding was
to prohibit nonlinear unbranched
  instances entirely. Unfortunately, that doesn't work. Consider this:

  type family H (x :: [k]) :: *
  type instance H '[] = Bool

  Innocent enough, it seems. However, that instance expands to type
instance H k ('[] k) = Bool internally.
  And that expansion contains a repeated variable! Yuck. We Thought
Hard about this and came up with
  various proposals to fix it, but we weren't convinced that any of
them were any good. So, we concluded
  to allow nonlinear unbranched instances, but we linearize them when
checking overlap. This may surprise
  some users, but we will put in a helpful error message in this case.

So in summary, if you extend the pattern with explicit kind info, you
get linearity for patterns that are actually fine.  It's not clear to
me why you would in fact use the expanded form when checking
linearity.  Wouldn't you get the same problem if you try to check a
value-level pattern's linearity after including explicit type info. If
so, why is that a problem for type instance patterns if it isn't a
problem for value-level patterns?

For example, take the following value-level function
  null :: [a] -> Bool
  null [] = True
  null (_:_) = False
After including explicit System F-like type arguments, that would become
  null @a ([] @a) = True
  null @a ((:) @a _ _) = False
So we get the same problem of non-linearity of the expansion even
though the original is fine, right?

Perhaps we could consider adding an internal annotation like the "@"
above on the arguments inserted by the expansion of a type instance
pattern with kinding info (or sort info if that's more correct?). Then
one could ignore those arguments altogether during the linearity
check.

Note: I'm in favor of avoiding non-linear patterns for type families
if at all possible, in order to keep the type-level computational
model functional and close to the value-leve one.  I would hope we
could forbid linear patterns for type classes as well at some point in
the future, although that could perhaps be more controversial still...

Thanks!
Dominique

P.S.: I hope you'll be writing a more detailed account of this work (a
research paper?) at some point and I look forward to reading it...

P.S.2: On an unrelated note: will you also do a completeness check on
closed type family definitions?

2013/5/29 Richard Eisenberg <eir at cis.upenn.edu>:
> (Sorry for the re-send – got the wrong subject line last time.)
>
>
>
> Hello all,
>
>
>
> It’s come to my attention that there is a tiny lurking potential hole in
> GHC’s type safety around type families in the presence of
> UndecidableInstances. Consider the following:
>
>
>
>> type family F a b
>
>> type instance F x x = Int
>
>> type instance F [x] x = Bool
>
>>
>
>> type family G
>
>> type family G = [G]
>
>
>
> This declarations are all valid in GHC 7.6.3. However, depending on the
> reduction strategy used, it is possible to reduce `F G G` to either Int or
> Bool. I haven’t been able to get this problem to cause a seg-fault in
> practice, but I think that’s more due to type families’ strictness than
> anything more fundamental. Thus, we need to do something about it.
>
>
>
> I have written a proposal on the GHC wiki at
> http://hackage.haskell.org/trac/ghc/wiki/NewAxioms/Nonlinearity
>
>
>
> It proposes a change to the syntax for branched instances (a new form of
> type family instance that allows for ordered matching), but as those haven’t
> yet been officially released (only available in HEAD), I’m not too worried
> about it.
>
>
>
> There are two changes, though, that break code that compiles in released
> versions of GHC:
>
> ---
>
> 1) Type family instances like the two for F, above, would no longer be
> accepted. In particular, the overlap check for unbranched (regular
> standalone instances like we’ve had for years) would now check for overlap
> if all variables were distinct. (This freshening of variables is called
> ‘linearization’.) Thus, the check for F would look at `F x y` and `F [x] y`,
> which clearly overlap and would be conflicting.
>
>
>
> 2) Coincident overlap between unbranched instances would now be prohibited.
> In the new version of GHC, these uses of coincident overlap would have to be
> grouped in a branched instance. This would mean that all equations that
> participate in coincident overlap would have be defined in the same module.
> Cross-module uses of coincident overlap may be hard to refactor.
>
> ---
>
>
>
> Breaking change #1 is quite necessary, as that’s the part that closes the
> hole in the type system.
>
> Breaking change #2 is strongly encouraged by the fix to #1, as the
> right-hand side of an instance is ill-defined after the left-hand side is
> linearized. It is conceivable that there is some way to recover coincident
> overlap on unbranched instances, but it’s not obvious at the moment. Note
> that this proposal does not contain a migration path surrounding coincident
> overlap. In GHC <= 7.6.x, branched instances don’t exist and we have
> coincident overlap among unbranched instances; and in GHC >= 7.8.x, we will
> prohibit coincident overlap except within branched instances. We (Simon PJ
> and I) think that this shouldn’t be too big of a problem, but please do
> shout if it would affect you.
>
>
>
> Please let me know what you think about this proposal!
>
>
>
> Thanks,
>
> Richard
>
>
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>