Fix #13333 by fixing the covar's type in ctEvCoercion

The change is noted in Note [Given in ctEvCoercion]. This patch
also adds a bit more commentary to TcFlatten, documenting some
key invariants of the flattening algorithm. While in the area,
I also removed some stale commentary from TcCanonical.

2 files changed, 29 insertions, 0 deletions

diff --git a/testsuite/tests/typecheck/should_compile/T13333.hs b/testsuite/tests/typecheck/should_compile/T13333.hs
new file mode 100644
index 0000000000..fba64cede0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T13333.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T13333 where
+
+import Data.Data
+import GHC.Exts (Constraint)
+
+data T (phantom :: k) = T
+
+data D (p :: k -> Constraint) (x :: j) where
+  D :: forall (p :: k -> Constraint) (x :: k). p x => D p x
+
+class Possibly p x where
+  possibly :: proxy1 p -> proxy2 x -> Maybe (D p x)
+
+dataCast1T :: forall k c t (phantom :: k).
+              (Typeable k, Typeable t, Typeable phantom, Possibly Data phantom)
+           => (forall d. Data d => c (t d))
+           -> Maybe (c (T phantom))
+dataCast1T f = case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
+                 Nothing -> Nothing
+                 Just D  -> gcast1 f
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 67fe104155..874235387e 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -556,3 +556,4 @@ test('T13524', normal, compile, [''])
 test('T13509', normal, compile, [''])
 test('T13526', normal, compile, [''])
 test('T13603', normal, compile, [''])
+test('T13333', normal, compile, [''])