1 files changed, 73 insertions, 0 deletions
diff --git a/testsuite/tests/dependent/should_compile/LopezJuan.hs b/testsuite/tests/dependent/should_compile/LopezJuan.hs
new file mode 100644
index 0000000000..bc7cc89201
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/LopezJuan.hs
@@ -0,0 +1,73 @@
+{-
+
+This test is inspired by
+  Practical dependent type checking using twin types
+  Victor López Juan and Nils Anders Danielsson
+  TyDe '20
+  https://dl.acm.org/doi/10.1145/3406089.3409030
+
+The challenge is whether we can unify two types where the only
+way to know that the kinds are equal is to unify the types. This
+would fail in an algorithm that required kind unification before
+type unification.
+-}
+
+{-# LANGUAGE TypeOperators, TypeApplications, DataKinds,
+             StandaloneKindSignatures, PolyKinds, GADTs,
+             TypeFamilies, NamedWildCards, PartialTypeSignatures #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
+
+module LopezJuan where
+
+import Data.Type.Equality ( (:~~:)(..) )
+import Data.Kind ( Type )
+import Data.Proxy ( Proxy )
+
+-- amazingly, this worked without modification
+
+data SBool :: Bool -> Type where
+  SFalse :: SBool False
+  STrue  :: SBool True
+
+data BoolOp where
+  None :: Bool -> BoolOp
+  Some :: Bool -> BoolOp
+
+type F :: Bool -> Type
+type family F b
+
+get :: BoolOp -> Bool
+get (None _) = True
+get (Some x) = x
+
+type Get :: BoolOp -> Bool
+type family Get x where
+  Get (None _) = True
+  Get (Some x) = x
+
+type TyFun :: Type -> Type -> Type
+data TyFun arg res
+
+type (~>) :: Type -> Type -> Type
+type arg ~> res = TyFun arg res -> Type
+infixr 0 ~>
+
+data Const :: a -> (b ~> a)
+
+f :: SBool x -> (:~~:) @(F (Get (_alpha x)) ~> BoolOp)
+                       @(F True ~> BoolOp)
+                       (Const (None x))
+                       (Const (_alpha x))
+f _ = HRefl
+
+-- and something simpler:
+
+type family Idish guard a where
+  Idish True a = a
+  Idish False a = Int
+
+g :: (:~~:) @(Idish _alpha Type)
+            @Type
+            (Proxy _alpha)
+            (Proxy True)
+g = HRefl