@qnikst, Как понять "не будут выведены в конкрентый тип по S s a"

@fmap, ?

@fmap, т.е. если type infer будет происходить не по H s a
в смысле пусть есть foo :: H s Int, тогда если есть код
foo (hexp s) — то s выведется как `S s Int` чего я не хочу.

Но я хочу обратного если известно, что s :: S s Int, то hexp s точно будет foo s :: H s Int

@qnikst, Если только для определенных типов: hexp :: S s a -> H s (F a b); type family F a b :: *; type instance F A b = A; type instance F B b = B; ...; type instance F a b = b;

@fmap, ну вот я тоже подумал, что через тайпфемили и неиньективность можно (хотя тут кайнд MyType -> *, так что может и нету неиньективности)

@fmap, ещё можно фендепы попробовать :

class Foo a b | a -> b where .. тогда а не будет выводиться если известно b и наоборот b выводится, если известно a

@qnikst, В HM такого точно нельзя сделать.

@fmap, {-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
module Main where

class Foo a b | a -> b where
fooCoerce :: a -> b

instance Foo Int Int where fooCoerce = id
instance Foo Double Double where fooCoerce = id


newtype S a = S { unS :: a}
newtype H a = H { unH :: a}

foo :: Foo a b => S a -> H b
foo (S x) = H (fooCoerce x)

test1 = foo (S (3::Int))

test2 = case foo (S (3::Int)) of
H x -> (x + (1::Int))

— не компилируется
— test3 = case foo (S 3) of
— H x -> (x + (1::Int))

@qnikst, а вот с instance Foo a a where fooCoerce = id — компилируется

@qnikst, Тут та же проблема как в /4? А какой use case у /0?

@fmap, есть данные приходящие из FFI кода: S s a (грубо говоря враппер вокруг pointer), есть GADT (H s a) их описывающий с конструкторами для каждого конкретного a. Есть метод hexp :: S s a -> H s a, который работает примерно так:
unsafeInlinIO . . peek . unS, где peek это

peek :: Ptr (H s a) -> H s a
peek p = case typeOf p of
C1 -> unsafeCoerce $ realPeek (unsafeCoerce p)
....

в итоге эта байда сносит ghc крышу. Проблема тут в том, что а). мне кажется что в оптимизациях есть баг судя по генерируемым стейджам), б). 'a' не всегда выводится верно.

Для S есть экзестенциальный тип SomeS, который выдается когда настоящий S неизвестен, и там это спасает. Но тут как-то все хуже, у меня есть:

case (hexp . (cast :: SSINGTYPE a -> SomeSEXP s -> S s a) R.Int s) of
тут case повсем возможным веткам

так вот я думаю, как мы уменьшить ghc ум, чтобы он лишнего не выводил и ленюсь дебажить..

@qnikst, вот `case typeOf` с парой unsafeCoerce тут намекает на то, что нахрен все переписать надо...

@qnikst, а ещё про струкруру GADT, почти для всех типов это H s (ConcreteType), но есть пара конструктуров которые имеют тип `H s a`, это скорее всего важно здесь