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%7Cc333fbaff2f4406c337e08d4c3
| 3bd1bd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636348109082017989&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
