Trouble with injective type families

[Wolfgang Jeltsch]

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-
> > bounces at haskell.org] On Behalf Of Wolfgang Jeltsch
> > Sent: 05 July 2017 01:21
> > To: glasgow-haskell-users at 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 at 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