{-# LANGUAGE DataKinds, GADTs, UndecidableInstances, TypeFamilies #-}

data Nat = Z | S Nat

type family Infinite :: Nat where Infinite = S Infinite

data Vec (n :: Nat) where VZ :: Vec Z ; VS :: Vec n -> Vec (S n)

x :: Vec Infinite
x = VS x

main = main

{-
A.hs:10:5: error:
    • Reduction stack overflow; size = 201
      When simplifying the following type: Infinite
      Use -freduction-depth=0 to disable this check
      (any upper bound you could choose might fail unpredictably with
       minor updates to GHC, so disabling the check is recommended if
       you're sure that type checking should terminate)
    • In the expression: VS x
      In an equation for ‘x’: x = VS x
   |
10 | x = VS x
   |     ^^^^
-}