Stream: general

Topic: In what case these impls conflict?


nagisa (Apr 26 2019 at 00:53, on Zulip):

For this code https://play.rust-lang.org/?version=stable&mode=debug&edition=2018&gist=e584d0a9cc905d31aed9abcc3a23b8fa we report conflicting impls, however I have failed to think of a case where this would actually be a conflicting implementation.

centril (Apr 26 2019 at 00:57, on Zulip):

@nagisa those impls cannot overlap but rustc is too dumb to take into account that associated types are functions in terms of coherence

centril (Apr 26 2019 at 00:58, on Zulip):

@nagisa simplified: https://play.rust-lang.org/?version=stable&mode=debug&edition=2018&gist=3da3b94fd735979884440d4f3ca9fbf8

nagisa (Apr 26 2019 at 01:00, on Zulip):

That simplification looks alpha-equivalent to me :slight_smile:

nagisa (Apr 26 2019 at 01:01, on Zulip):

is making rust to understand this something we want to do?

kennytm (Apr 26 2019 at 01:02, on Zulip):

https://github.com/rust-lang/rfcs/pull/1672 (postponed)

nagisa (Apr 26 2019 at 01:04, on Zulip):

Aww.

centril (Apr 26 2019 at 01:04, on Zulip):

@nagisa do you remember what GHC does?

nagisa (Apr 26 2019 at 01:04, on Zulip):

I do not. I never hit this back when I was using Haskell at least.

centril (Apr 26 2019 at 01:13, on Zulip):
{-# LANGUAGE TypeFamilies, FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-} -- oh noes!

class X a where type F a :: *
class X a => Y a where
data A = A
data B = B
instance (X i, A ~ F i) => Y i where
instance (X i, B ~ F i) => Y i where

@nagisa GHC 8.0.2 accepts this ^---

centril (Apr 26 2019 at 01:15, on Zulip):

tho I should check with a newer version to make sure it still holds

centril (Apr 26 2019 at 01:20, on Zulip):

Explanatory notes for those who are not Haskell proficient:
1. class ==> trait;
2. the Self type is the first type variable in the class.
3. type F a :: * denotes an associated type F that when given type a projects to a type of kind * (concrete types)
4. X a => Y a denotes a super class constraint (to implement Y for a you must also implement X for a)
5. data A = A is the same as struct A;
6. instance Ctx => Class Type denotes that you are defining an implementation of Class for Type provided that Ctx holds.
7. Alpha ~ Beta is a type equality constraint

centril (Apr 26 2019 at 01:22, on Zulip):

8. Type variables in Haskell are lowerCamelCased, concrete types are UpperCamelCased; Haskell implicitly quantifies type variables by default

Last update: Nov 22 2019 at 00:30UTC