Re: Trouble with injective type families

6 Jul 2017

      ...
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.
...
...
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 dont provide evidence.  That's not to say
...
...
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
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-31297455...

AntC

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

Anthony Clayden

tags

participants (1)