Test Trac #10226

Fixed by the patch for #10009

2 files changed, 60 insertions, 1 deletions

diff --git a/testsuite/tests/indexed-types/should_compile/T10226.hs b/testsuite/tests/indexed-types/should_compile/T10226.hs
new file mode 100644
index 0000000000..947429d37a
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T10226.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE AllowAmbiguousTypes #-} -- only necessary in 7.10
+{-# LANGUAGE FlexibleContexts #-}    -- necessary for showFromF' example
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
+
+module T10226 where
+
+type family F    a
+type family FInv a
+
+-- This definition is accepted in 7.8 without anything extra, but requires
+-- AllowAmbiguousTypes in 7.10 (this, by itself, is not a problem):
+showFromF :: (Show a, FInv (F a) ~ a) => F a -> String
+showFromF fa = undefined
+
+-- Consider what happens when we attempt to call `showFromF` at some type b.
+-- In order to check that this is valid, we have to find an a such that
+--
+-- > b ~ F a /\ Show a /\ FInv (F a) ~ a
+--
+-- Introducing an intermeidate variable `x` for the result of `F a` gives us
+--
+-- > b ~ F a /\ Show a /\ FInv x ~ a /\ F a ~ x
+--
+-- Simplifying
+--
+-- > b ~ x /\ Show a /\ FInv x ~ a /\ F a ~ x
+--
+-- Set x := b
+--
+-- > Show a /\ FInv b ~ a /\ F a ~ b
+--
+-- Set a := FInv b
+--
+-- > Show (FInv b) /\ FInv b ~ FInv b /\ F (FInv b) ~ b
+--
+-- Simplifying
+--
+-- > Show (FInv b) /\ F (FInv b) ~ b
+--
+-- Indeed, we can give this definition in 7.8, but not in 7.10:
+showFromF' :: (Show (FInv b), F (FInv b) ~ b) => b -> String
+showFromF' = showFromF
+
+{-------------------------------------------------------------------------------
+  In 7.10 the definition of showFromF' is not accepted, but it gets stranger.
+  In 7.10 we cannot _call_ showFromF at all all, even at a concrete type. Below
+  we try to call it at type b ~ Int. It would need to show
+
+  > Show (FInv Int) /\ F (FInt Int) ~ Int
+
+  all of which should easily get resolved, but somehow don't.
+-------------------------------------------------------------------------------}
+
+type instance F    Int = Int
+type instance FInv Int = Int
+
+test :: String
+test = showFromF (0 :: Int)
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 1cd1ea261a..20f2c0a07b 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -254,4 +254,4 @@ test('T10020', normal, compile, [''])
 test('T10079', normal, compile, [''])
 test('T10139', normal, compile, [''])
 test('T10340', normal, compile, [''])
-
+test('T10226', normal, compile, [''])