Trouble with injective type families

[Anthony Clayden]

> On Wed Jul 5 14:16:10 UTC 2017, Richard Eisenberg wrote:

> I'd like to add that the reason we never extended System
FC
> with support for injectivity is that the proof of
soundness
> of doing so has remained elusive.

Thank you Richard, Simon.

IIRC the original FDs through CHRs paper did think it sound
to allow given `C a b1` and `C a b2` conclude `b1 ~ b2`
under a FunDep `a -> b`.
(I think that was also the case in Mark Jones'
 original paper on FunDeps.)

(See Iavor's comments on Trac #10675, for example.)

I know GHC's current FunDep inference is lax,
because there's good reasons to want 'wiggle room'
with FunDep (in)consistency.

I'm suggesting we could tighten that consistency check;
then we might make make FD inference stronger(?)
https://github.com/ghc-proposals/ghc-proposals/pull/56#issuecomment-312974557


AntC

>> 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?
>>>