GHC hanging

[RafaelBocquet]

Here is an example hanging the compiler :

{-# LANGUAGE GADTs, TypeFamilies, TypeOperators, DataKinds,
             PolyKinds, RankNTypes, ScopedTypeVariables #-}

module A where

data N = Z | S N

data Fin n where
  FZ :: Fin (S n)
  FS :: Fin n -> Fin (S n)

data SFin (n :: N) (f :: Fin n) where
  SFZ :: SFin (S n) FZ
  SFS :: SFin n f -> SFin (S n) (FS f)

type family Minus n (i :: Fin n) :: N where
  Minus (S n) FZ     = S n
  Minus (S n) (FS i) = Minus n i

data A (n :: N) = forall i. B (SFin n i) (A (Minus n i))

type family F (a :: A n) :: A n where
  F (B i a) = B i (F a) 

Also, ghc can panic when an argument to a type constructor is forgotten. (e.g. with data A (n :: N) = forall i. B (SFin n i) A).

Attempting to replace type families with type classes panics : visible binder in tcInstBinderX [anon] Minus n_am0 i_am1 m_am2

{-# LANGUAGE GADTs, TypeFamilies, TypeOperators, DataKinds,
             PolyKinds, RankNTypes, ScopedTypeVariables,
             MultiParamTypeClasses, FunctionalDependencies #-}

module A where

data N = Z | S N

data Fin (n :: N) where
  FZ :: Fin (S n)
  FS :: Fin n -> Fin (S n)

data SFin (n :: N) (f :: Fin n) where
  SFZ :: SFin (S n) FZ
  SFS :: SFin n f -> SFin (S n) (FS f)

class Minus (n :: N) (i :: Fin n) (m :: N) | n i -> m

data A (n :: N) = forall (i :: Fin n) (m :: N). Minus n i m => B (SFin n i) (A m)

class RA (a :: A n)
instance RA (B i a)