Type families: Tricky GADT/RankN/TF example

testsuite/tests/ghc-regress/indexed-types/should_compile/GADT14.hs

+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs,  RankNTypes, FlexibleContexts #-}
+module Equality( (:=:), eq_elim, eq_refl ) where
+
+data a:=: b where
+  EQUAL :: a :=: a
+
+eq_refl :: a :=: a
+eq_refl = EQUAL
+
+eq_elim :: (a~b) => a :=: b -> (a~b => p) -> p
+eq_elim EQUAL p = p 

testsuite/tests/ghc-regress/indexed-types/should_compile/all.T

@@ -69,6 +69,7 @@ test('GADT10', expect_fail, compile, [''])
 test('GADT11', normal, compile, [''])
 test('GADT12', expect_fail, compile, [''])
 test('GADT13', expect_fail, compile, [''])
+test('GADT14', normal, compile, [''])
 
 test('Class1', normal, compile, [''])
 test('Class2', normal, compile, [''])