Type-level GADT inference failure (?)

{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, PolyKinds, DataKinds,
             NoImplicitPrelude, UndecidableInstances, RankNTypes, TemplateHaskell #-}
{-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}

module Part5a where

import Prelude ( Bool(..), return )
import GHC.TypeLits ( type (-) )
import Data.Type.Bool

data Nat :: * where
  Zero :: Nat
  Succ :: Nat -> Nat

data family Sing (a :: k)

data instance Sing (n :: Nat) where
  SZero :: Sing 'Zero
  SSucc :: Sing n -> Sing ('Succ n)

data instance Sing (t :: *) where
  SNat  :: Sing Nat
  SBool :: Sing Bool

(+) :: Nat -> Nat -> Nat
Zero   + m = m
Succ n + m = Succ (n + m)
infixl 6 +

type family a :+ b where
  'Zero :+ m = m
  'Succ n :+ m = 'Succ (n :+ m)

(%:+) :: Sing a -> Sing b -> Sing (a :+ b)
SZero %:+ m = m
SSucc n %:+ m = SSucc (n %:+ m)

data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *

$(return [])

data Expr :: Sing (a :: *) -> * where
  Val  :: forall (t :: *) (st :: Sing t). t -> Expr st
  Plus :: Expr 'SNat -> Expr 'SNat -> Expr 'SNat
  If   :: Expr 'SBool -> Expr t -> Expr t -> Expr t

data instance Sing (e :: Expr t) where
  SVal  :: Sing t -> Sing ('Val t)
  SPlus :: Sing a -> Sing b -> Sing ('Plus a b)
  SIf   :: Sing b -> Sing t -> Sing f -> Sing ('If b t f)

type SExpr (e :: Expr t) = Sing e

eval :: forall (t :: *) (st :: Sing t). Expr st -> t
eval (Val n)        = n
eval (e1 `Plus` e2) = eval e1 + eval e2
eval (If e0 e1 e2)  = if eval e0 then eval e1 else eval e2

type family Eval (x :: Expr (st :: Sing t)) :: t where
  Eval ('Val n) = n
  Eval ('Plus e1 e2) = Eval e1 :+ Eval e2

--  Eval ('If e0 e1 e2) = If (Eval e0) (Eval e1) (Eval e2)
{-
sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)
sIf SFalse _ c = c
sIf STrue  b _ = b

sEval :: SExpr e -> Sing (Eval e)
sEval (SVal n) = n
sEval (e1 `SPlus` e2) = sEval e1 %:+ sEval e2
sEval (SIf e0 e1 e2) = sIf (sEval e0) (sEval e1) (sEval e2)

type family U n where
  U 0 = 'Zero
  U n = 'Succ (U (n-1))

type Rel i = i -> i -> *

data List (x :: Rel i) :: Rel i where
  Nil   :: List x i i
  (:::) :: x i j -> List x j k -> List x i k
infixr 5 :::

(++) :: List x i j -> List x j k -> List x i k
Nil ++ ys = ys
(x ::: xs) ++ ys = x ::: (xs ++ ys)
infixr 5 ++

type SC = [*]

data Elt :: Rel SC where
  E :: t -> Elt (t ': ts) ts

type Stk i = List Elt i '[]

data StkSym0 :: SC ~> *
type family (f :: a ~> b) @@ (x :: a) :: b
type instance StkSym0 @@ x = Stk x

data instance Sing (a :: [k]) where
  SNil :: Sing '[]
  SCons :: Sing h -> Sing t -> Sing (h ': t)
infixr 5 `SCons`

data instance Sing (a :: Bool) where
  SFalse :: Sing 'False
  STrue :: Sing 'True
-}

leads to

Part5a.hs:62:9:
    Couldn't match expected kind ‘t’ with actual kind ‘Nat’
    In the first argument of ‘Eval’, namely ‘Plus e1 e2’
    In the type family declaration for ‘Eval’

I think that's bogus, because we should be able to unify t with Nat.

goldfirere / ghc

Type-level GADT inference failure (?) #13