Почему GHC не уменьшит мою семью?

Question

Вот нетипизированное лямбда-исчисление, члены которого индексируются по их свободным переменным. Я использую библиотеку singletons для одноточечных значений строк уровня.

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE PolyKinds #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE UndecidableInstances #-} 

import Data.Singletons 
import Data.Singletons.TypeLits 

data Expr (free :: [Symbol]) where 
    Var :: Sing a -> Expr '[a] 
    Lam :: Sing a -> Expr as -> Expr (Remove a as) 
    App :: Expr free1 -> Expr free2 -> Expr (Union free1 free2) 

A Var вводит свободную переменную. Абстракция лямбда связывает переменную, которая кажется свободной в теле (если есть та, которая соответствует). Приложения объединяют свободные переменные двух частей выражения, удаляя дубликаты (поэтому свободные переменные x y: x и y, а свободные переменные x x - это всего лишь x). Я выписал те семьи, типа:

type family Remove x xs where 
    Remove x '[] = '[] 
    Remove x (x ': xs) = Remove x xs 
    Remove x (y ': xs) = y ': Remove x xs 

type family Union xs ys where 
    Union xs ys = Nub (xs :++ ys) 

type family xs :++ ys where 
    '[] :++ ys = ys 
    (x ': xs) :++ ys = x ': (xs :++ ys) 

type family Nub xs where 
    Nub xs = Nub' '[] xs 

type family Nub' seen xs where 
    Nub' seen '[] = '[] 
    Nub' seen (x ': xs) = If (Elem x seen) (Nub' seen xs) (Nub' (x ': seen) (x ': xs)) 

type family If c t f where 
    If True t f = t 
    If False t f = f 

type family Elem x xs where 
    Elem x '[] = False 
    Elem x (x ': xs) = True 
    Elem x (y ': xs) = Elem x xs 

Я испытал это на интерактивном режиме:

ghci> :t Var (sing :: Sing "x") 
Var (sing :: Sing "x") :: Expr '["x"] -- good 
ghci> :t (Lam (sing :: Sing "x") (Var (sing :: Sing "x"))) 
(Lam (sing :: Sing "x") (Var (sing :: Sing "x"))) 
    :: Expr (Remove "x" '["x"]) -- not so good 

Я был удивлен, узнав, что тип функции тождества \x. x является Expr (Remove "x" '["x"]), не Expr '[]. GHC, похоже, не хочет оценивать тип семейства Remove. Я экспериментировал немного больше, и узнал, что это не проблема с моим типом семьи в себе - GHC счастлив, чтобы уменьшить его в этом случае:

ghci> :t (Proxy :: Proxy (Remove "x" '["x"])) 
(Proxy :: Proxy (Remove "x" '["x"])) :: Proxy '[] 

Итак: Почему не GHC уменьшить Remove "x" '["x"] к '[], когда я запросить тип моего GADT? В общем, когда воля-или-не будет проверять тип семейства типов? Есть ли эвристика, которую я могу использовать, чтобы не удивляться ее поведению?

Answer 1

Это работает. Кажется, что GHC просто ленив.

λ *Main > :t (Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) 
(Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) 
    :: Expr (Remove "x" '["x"]) 

λ *Main > :t (Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) :: Expr '[] 
(Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) :: Expr '[] 
    :: Expr '[] 

λ *Main > :t (Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) :: Expr '["x"] 

<interactive>:1:2: 
    Couldn't match type ‘'[]’ with ‘'["x"]’ 
    Expected type: Expr '["x"] 
     Actual type: Expr (Remove "x" '["x"]) 
    In the expression: 
     (Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) :: 
      Expr '["x"] 

---

Я изменил определение, так что не зависим от библиотеки Singletons (проще тестировать в одноранговой сети):

{-# LANGUAGE TypeOperators, DataKinds, TypeFamilies, GADTs #-} 

import Data.Proxy 
import GHC.TypeLits 

type family Remove (x :: Symbol) (xs :: [Symbol]) where 
    Remove x '[] = '[] 
    Remove x (x ': xs) = Remove x xs 
    Remove x (y ': xs) = y ': Remove x xs 

data Expr (free :: [Symbol]) where 
    Var :: KnownSymbol a => Proxy a -> Expr '[a] 
    Lam :: KnownSymbol a => Proxy a -> Expr as -> Expr (Remove a as) 
-- App :: Expr free1 -> Expr free2 -> Expr (Union free1 free2)