Looping in System F encoding

This causes GHC to loop:

{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies,
             UndecidableInstances #-}
{-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}

module SystemF where

import Data.Type.Bool
import GHC.Exts ( Any )

data Nat = Zero | Succ Nat

type family Pred n where
  Pred ('Succ n) = n

data Fin n where
  FZ :: Fin ('Succ n)
  FS :: Fin n -> Fin ('Succ n)

type family (a :: x) <= (f :: Fin n) :: Bool where
  'Zero <= x       = 'True
  'FZ <= x         = 'True

  x  <= 'FZ         = 'False

  'Succ a <= 'FS b = a <= b
  'FS a   <= 'FS b = a <= b

type family FPred (f :: Fin n) :: Fin (Pred n) where
  FPred ('FS f) = f

type family BumpFin (f :: Fin n) :: Fin ('Succ n) where
  BumpFin 'FZ = 'FZ
  BumpFin ('FS f) = 'FS (BumpFin f)

type family BumpFinDown (f :: Fin n) :: Fin (Pred n) where
  BumpFinDown 'FZ = 'FZ
  BumpFinDown ('FS f) = 'FS (BumpFinDown f)

goldfirere / ghc

Looping in System F encoding #27