summaryrefslogtreecommitdiff
path: root/testsuite/tests/typecheck/should_compile/T13651.hs
blob: 63bd88eb5c28a9986bc4a17b2a8f0f3283bc3e9e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
{-# LANGUAGE TypeFamilies, TypeFamilyDependencies #-}
module T13651 where

type family F r s = f | f -> r s

type instance F (Bar h (Foo r)) (Bar h (Foo s)) = Bar h (Bar r s)

data Bar s b
data Foo a

foo :: (F cr cu ~ Bar h (Bar r u),
        F cu cs ~ Bar (Foo h) (Bar u s))
    => Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)
foo = undefined

{-  Typechecking this program used to /just/ succeed in GHC 8.2,
    (see Trac #14745 for why), but doesn't in 8.4.

[G]  F cr cu ~ Bar h (Bar r u),
     F cu cs ~ Bar (Foo h) (Bar u s))


[W] F cr cu0 ~ Bar h (Bar r u)
    --> (top-level fundeps)  cr ~ Bar h (Foo r)
                             cu0 ~ Bar h (Foo u)
        (local fundeps)      cu ~ cu0

[W] F cu0 cs ~ Bar (Foo h) (Bar u s)
    -->  (top-level fundeps)  cu0 ~ Bar (Foo h) (Foo u)
                              cs  ~ Bar (Foo h) (Foo s)
         (local fundeps)      cu0 ~ cu

[W] F cr (Bar (Foo h) (Fo u)) ~ Bar h (Bar r u)

-}