> 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 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 >>>> 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? >>> _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users