Dear Simon, thank you very much for this elaborate explanation.
I stumbled on this issue when using functional dependencies years ago. The solution at that time was to use type families. I did not know that injectivity is handled analogously to functional dependencies. Given that it is, the syntax for injectivity makes a lot more sense. All the best, Wolfgang Am Mittwoch, den 05.07.2017, 06:45 +0000 schrieb Simon Peyton Jones: > Functional dependencies and type-family dependencies only induce extra > "improvement" constraints, not evidence. For example > > class C a b | a -> b where foo :: a -> b > instance C Bool Int where ... > > f :: C Bool b => b -> Int > f x = x -- Rejected > > Does the fundep on 'b' allow us to deduce (b ~ Int), GADT-like, in the > body of 'f', and hence accept the definition. No, it does not. Think > of the translation into System F. We get > > f = /\b \(d :: C Bool b). \(x::b). x |> ??? > > What evidence can I used to cast 'x' by to get it from type 'b' to > Int? > > Rather, fundeps resolve ambiguity. Consider > > g x = foo True + x > > The call to 'foo True' gives rise to a "wanted" constraint (C Bool > beta), where beta is a fresh unification variable. Then by the fundep > we get an "improvement" constraint (also "wanted") (beta ~ Int). So we > can infer g :: Int -> Int. > > > In your example we have > > x :: forall a b. (T Int ~ b) => a > x = False > > Think of the System F translation: > > x = /\a b. \(d :: T Int ~ b). False |> ?? > > Again, what evidence can we use to cast False to 'a'. > > > In short, fundeps and type family dependencies only add extra > unification constraints, which may help to resolve ambiguous > types. They don’t provide evidence. That's not to say that they > couldn't. But you'd need to extend System FC, GHC's core language, to > do so. > > Simon > > > > > > -----Original Message----- > > From: Glasgow-haskell-users [mailto:glasgow-haskell-users- > > boun...@haskell.org] On Behalf Of Wolfgang Jeltsch > > Sent: 05 July 2017 01:21 > > To: glasgow-haskell-users@haskell.org > > Subject: Trouble with injective type families > > > > Hi! > > > > Injective type families as supported by GHC 8.0.1 do not behave like > > I > > would expect them to behave from my intuitive understanding. > > > > Let us consider the following example: > > > > > > > > {-# LANGUAGE RankNTypes, TypeFamilyDependencies #-} > > > > > > class C a where > > > > > > type T a = b | b -> a > > > > > > instance C Bool where > > > > > > type T Bool = Int > > > > > > type X b = forall a . T a ~ b => a > > > > > > x :: X Int > > > x = False > > I would expect this code to be accepted. However, I get the > > following > > error message: > > > > > > > > A.hs:14:5: error: > > > • Could not deduce: a ~ Bool > > > from the context: T a ~ Int > > > bound by the type signature for: > > > x :: T a ~ Int => a > > > at A.hs:13:1-10 > > > ‘a’ is a rigid type variable bound by > > > the type signature for: > > > x :: forall a. T a ~ Int => a > > > at A.hs:11:19 > > > • In the expression: False > > > In an equation for ‘x’: x = False > > > • Relevant bindings include x :: a (bound at A.hs:14:1) > > This is strange, since injectivity should exactly make it possible > > to > > deduce a ~ Bool from T a ~ Int. > > > > Another example is this: > > > > > > > > {-# LANGUAGE GADTs, TypeFamilyDependencies #-} > > > > > > class C a where > > > > > > type T a = b | b -> a > > > > > > instance C Bool where > > > > > > type T Bool = Int > > > > > > data G b where > > > > > > G :: Eq a => a -> G (T a) > > > > > > instance Eq (G b) where > > > > > > G a1 == G a2 = a1 == a2a > > I would also expect this code to be accepted. However, I get the > > following error message: > > > > > > > > B.hs:17:26: error: > > > • Could not deduce: a1 ~ a > > > from the context: (b ~ T a, Eq a) > > > bound by a pattern with constructor: > > > G :: forall a. Eq a => a -> G (T a), > > > in an equation for ‘==’ > > > at B.hs:17:5-8 > > > or from: (b ~ T a1, Eq a1) > > > bound by a pattern with constructor: > > > G :: forall a. Eq a => a -> G (T a), > > > in an equation for ‘==’ > > > at B.hs:17:13-16 > > > ‘a1’ is a rigid type variable bound by > > > a pattern with constructor: G :: forall a. Eq a => a -> G > > > (T > > > a), > > > in an equation for ‘==’ > > > at B.hs:17:13 > > > ‘a’ is a rigid type variable bound by > > > a pattern with constructor: G :: forall a. Eq a => a -> G > > > (T > > > a), > > > in an equation for ‘==’ > > > at B.hs:17:5 > > > • In the second argument of ‘(==)’, namely ‘a2’ > > > In the expression: a1 == a2 > > > In an equation for ‘==’: (G a1) == (G a2) = a1 == a2 > > > • Relevant bindings include > > > a2 :: a1 (bound at B.hs:17:15) > > > a1 :: a (bound at B.hs:17:7) > > If b ~ T a and b ~ T a1, then T a ~ T a1 and subsequently a ~ a1, > > because > > of injectivity. Unfortunately, GHC does not join the two contexts (b > > ~ T > > a, Eq a) and (b ~ T a1, Eq a1). > > > > Are these behaviors really intended, or are these bugs showing up? > > > > All the best, > > Wolfgang > > _______________________________________________ > > Glasgow-haskell-users mailing list > > Glasgow-haskell-users@haskell.org > > https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail > > .hask > > ell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell- > > users&data=02%7C01%7Csimonpj%40microsoft.com%7Cc333fbaff2f4406c337e0 > > 8d4c3 > > 3bd1bd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6363481090820179 > > 89&sd > > ata=q%2B8ZSqYfNjC7x6%2Bm9vpsgCmCDo%2FIItppqB5Nwzf6Qj0%3D&reserved=0 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users