> 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 + 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 dont 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
