This produces (almost) 5000 lines of type error

LongTypeError.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

module LongTypeError where

import Data.Singletons.Prelude

data Data f where
  DataCon :: (a -> b) -> Data (a -> b)

function :: f -> Data f
function = undefined

type family TypeFam f fun where
  TypeFam f (a -> b) = f a -> TypeFam f b

lift :: forall f fun . fun -> TypeFam f fun
lift fun = case function fun of
  DataCon f -> \x -> _ (f <*> x)