Y-combinator

The Y-combinator in System F₂

:{
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
omega :: (forall a. a) -> (forall a. a)
omega x = x x

w :: (forall a. a) -> (forall a. a -> a) -> (forall a. a -> a)
w f x = f (x x)

y :: (forall a. a) -> _
y f =
  let x :: forall a. (forall b. b -> b) -> a -> a
      x = (w f)
      foo = x @(forall a. a -> a)
  in _
:}