Можно ли заменить универсальный и экзистенциальный квантификатор конструктора при сопоставлении с образцом?

Question

Вот фрагмент, который, на мой взгляд, имеет смысл (напечатайте), но который gh c не нравится. Я надеялся, что какое-то хитрое использование аннотаций типов может заставить его работать, но мои эксперименты не увенчались успехом. Есть какие-то предложения?

Answer 1

Я пробовал этот пример в Agda, чтобы увидеть, имеет ли он смысл

module Comm where

open import Data.Bool using (Bool; true)

record T (A : Set) : Set₁ where
  constructor MkT
  field
    F : Set → Set
    f : F A → A

bar : {F : Set → Set} → (∀ A → F A → A) → Bool
bar _ = true

foo : (∀ A → T A) → Bool
foo k = bar {F = k Bool .T.F} λ A → {!k A .T.f!}
-- Goal: k Bool .T.F A → A
-- Have: T.F. (k A) A → A

В foo нам нужно создать экземпляр forall a. T a с некоторым типом. Так как типом является параметр c, подойдет любой, и F будет таким же. Но ни в Agda, ни в Haskell нет встроенных параметров.

Так что я думаю, что при правильном использовании unsafeCoerce все будет работать.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# LANGUAGE TypeApplications #-}
module Ex where

import Unsafe.Coerce (unsafeCoerce)
import Data.List.NonEmpty (NonEmpty (..))
import GHC.Exts (Any)

data T a where
  T :: Functor f => (f a -> a) -> T a

bar :: Functor f => (forall a . f a -> a) -> Bool
bar _f = _f `seq` True

foo :: (forall a . T a) -> Bool
foo t = foo' t t

foo' :: (forall a. T a) -> T Any -> Bool
foo' t (T f) = aux f where
    aux :: forall f. Functor f => (f Any -> Any) -> Bool
    aux f' = bar f''
      where
        f'' :: forall a. f a -> a
        f'' = unsafeCoerce f'

--- test

ex :: forall a. T a
ex = T (\(x :| _) -> x)

ex2 :: Bool
ex2 = foo ex