1 files changed, 115 insertions, 0 deletions
diff --git a/testsuite/tests/dependent/should_fail/T13135_simple.hs b/testsuite/tests/dependent/should_fail/T13135_simple.hs
new file mode 100644
index 0000000000..576b923886
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13135_simple.hs
@@ -0,0 +1,115 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T13135_simple where
+
+import Data.Kind (Type)
+import GHC.Exts ( RuntimeRep(BoxedRep), Levity(Lifted) )
+
+{-
+NB: All the type applications and explicit quantification
+aren't necessary for the error
+to trigger, but they are helpful in reading this code.
+-}
+
+type Sig :: Type -> Type
+data Sig a = SigFun a (Sig a)
+-- SigFun :: forall (a :: Type). a -> Sig a -> Sig a
+
+type SmartFun :: forall (t :: Type). Sig t -> Type
+type family SmartFun sig = r | r -> sig where
+  forall (a :: Type) (sig :: Sig Type).
+    SmartFun @Type (SigFun @Type a sig) = a -> SmartFun @Type sig
+
+smartSym :: forall (k :: Type) (sig :: Sig k). SmartFun @k sig
+smartSym = error @(BoxedRep Lifted) @(SmartFun @k sig) "urk"
+
+problem :: Int -> Bool
+problem = smartSym
+
+{-
+problem arises in RHS of `problem`:
+
+instantiate smartSym:
+  kappa :: Type
+  sigma :: Sig kappa
+  smartSym :: SmartFun @kappa sigma
+
+[W] w1 :: SmartFun @kappa sigma ~ Int -> Bool
+
+injective type family says:
+beta :: Sig Type
+[W] w2 :: Type ~ kappa
+[W] w3 :: sigma ~ SigFun @Type Int beta
+
+then we have
+inert: [W] w1 :: SmartFun @kappa sigma ~ Int -> Bool
+work list: [W] w3 :: (SigFun @Type Int beta :: Sig Type) ~ (sigma :: Sig kappa)  (current item)
+           [W] w2 :: Type ~ kappa
+
+this is a hetero equality. So we get
+[W] w4 :: Type ~ kappa
+[W] w5 :: sigma ~ (SigFun @Type Int beta |> Sig w4)
+w3 is solved
+we cannot solve w5 by unification because of the coercion hole w4, so w5 becomes an inert,
+  kicking out w1
+
+next step.
+inert: [W] w5 :: sigma ~ (SigFun @Type Int beta |> Sig w4)
+work list: [W] w1 :: SmartFun @kappa sigma ~ Int -> Bool  (current item)
+           [W] w4 :: Type ~ kappa
+           [W] w2 :: Type ~ kappa
+
+LHS of w1 is rewritten, making it become
+  [W] w1 :: SmartFun @kappa (SigFun @Type Int beta |> Sig w4) ~ Int -> Bool
+
+injective type family says:
+gamma :: Sig Type
+[W] w6 :: Type ~ kappa
+[W] w7 :: (SigFun @Type Int gamma :: Sig Type)
+            ~
+          ((SigFun @Type Int beta |> Sig w4) :: Sig kappa)
+
+next step.
+inert: [W] w5 :: sigma ~ (SigFun @Type Int beta |> Sig w4)
+       [W] w1 :: SmartFun @kappa (SigFun @Type int beta |> Sig w4) ~ Int -> Bool
+work list: [W] w7 :: SigFun @Type Int gamma ~ (SigFun @Type Int beta |> Sig w4)  (current item)
+           [W] w6 :: Type ~ kappa
+           [W] w4 :: Type ~ kappa
+           [W] w2 :: Type ~ kappa
+
+we drop the cast on the work item, to get
+  [W] w7 :: SigFun @Type Int gamma ~ SigFun @Type Int beta
+this decomposes to
+  [W] w8 :: beta ~ gamma
+which gets added to the work list
+
+next step.
+inert: [W] w5 :: sigma ~ (SigFun @Type Int beta |> Sig w4)
+       [W] w1 :: SmartFun @kappa (SigFun @Type int beta |> Sig w4) ~ Int -> Bool
+work list: [W] w8 :: beta ~ gamma  (current item)
+           [W] w6 :: Type ~ kappa
+           [W] w4 :: Type ~ kappa
+           [W] w2 :: Type ~ kappa
+
+unify beta := gamma
+kick out w5 and w1
+
+next step.
+inert: none
+work list: [W] w5 :: sigma ~ (SigFun @Type Int beta |> Sig w4)   (current item)
+           [W] w1 :: SmartFun @kappa (SigFun @Type Int beta |> Sig w4) ~ Int -> Bool
+           [W] w6 :: Type ~ kappa
+           [W] w4 :: Type ~ kappa
+           [W] w2 :: Type ~ kappa
+
+w5 still cannot be solved by unification, and then when we see w1 again, we spit out
+new type-family injectivity equalities... and around and around we go.
+
+-}