Type-level GADT inference failure

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

module SystemF where

import Data.Type.Bool
import GHC.Exts ( Any )
import Data.Type.Equality

type family a ++ b where
  '[] ++ xs2 = xs2
  (x ': xs1) ++ xs2 = x ': (xs1 ++ xs2)
infixr 5 ++

data Nat = Zero | Succ Nat

type family Pred n where
  Pred ('Succ n) = n

data Fin n where
  FZ :: Fin ('Succ n)
  FS :: Fin n -> Fin ('Succ n)

type family (a :: x) <= (f :: Fin n) :: Bool where
  'Zero <= x       = 'True
  'FZ <= x         = 'True

  x  <= 'FZ         = 'False

  'Succ a <= 'FS b = a <= b
  'FS a   <= 'FS b = a <= b

type family (a :: Nat) `NPlus` (b :: Nat) where
  'Zero `NPlus` b = b
  'Succ a `NPlus` b = 'Succ (a `NPlus` b)

type family (a :: Nat) + (f :: Fin n) :: Fin (a `NPlus` n) where
  'Zero + f = f
  'Succ a + f = 'FS (a + f)

type family FPred (f :: Fin ('Succ n)) :: Fin n where
  FPred ('FS f) = f

type family WeakenFin (f :: Fin n) :: Fin ('Succ n) where
  WeakenFin 'FZ = 'FZ
  WeakenFin ('FS f) = 'FS (WeakenFin f)

type family WeakenFinN (n :: Nat) (f :: Fin m) :: Fin (n `NPlus` m) where
  WeakenFinN 'Zero f = f
  WeakenFinN ('Succ n) f = WeakenFin (WeakenFinN n f)

type family StrengthenFin (f :: Fin ('Succ n)) :: Fin n where
  StrengthenFin 'FZ = 'FZ
  StrengthenFin ('FS f) = 'FS (StrengthenFin f)

data SFin :: Fin n -> * where
  SFZ :: SFin 'FZ
  SFS :: SFin n -> SFin ('FS n)

data Ty n where
  TVar :: Fin n -> Ty n
  TForall :: Ty ('Succ n) -> Ty n
  (:~>) :: Ty n -> Ty n -> Ty n
infixr 0 :~>

data STy :: Ty n -> * where
  STVar :: SFin n -> STy ('TVar n)
  STForall :: STy ty -> STy ('TForall ty)
  (:%~>) :: STy t1 -> STy t2 -> STy (t1 ':~> t2)
infixr 0 :%~>

data Elem :: [a] -> a -> * where
  EZ :: Elem (x ': xs) x
  ES :: Elem xs x -> Elem (y ': xs) x

type family NPlus_Succ_R' (a :: Nat) (b :: Nat) (eq :: (a `NPlus` 'Succ b) :~: ('Succ (a `NPlus` b))) :: (('Succ a `NPlus` 'Succ b) :~: ('Succ ('Succ (a `NPlus` b)))) where
  NPlus_Succ_R' a b 'Refl = 'Refl

type family NPlus_Succ_R (a :: Nat) (b :: Nat) :: (a `NPlus` 'Succ b) :~: 'Succ (a `NPlus` b) where
  NPlus_Succ_R 'Zero b = 'Refl
--  NPlus_Succ_R ('Succ a) b = 'Refl

type family TShift (cutoff :: Nat) (shift :: Nat) (ty :: Ty n) :: Ty (shift `NPlus` n) where
  TShift cutoff shift ('TVar f)
    = If (cutoff <= f) ('TVar (shift + f)) ('TVar (WeakenFinN shift f))
--  TShift cutoff shift ('TForall ty) = 'TForall (TShift ('Succ cutoff) shift ty)
--  TShift cutoff shift (a ':~> b) = (TShift shift cutoff a) ':~> (TShift shift cutoff b)
{-
type family TShiftCtx (shift :: Nat) (tys :: [Ty n]) :: [Ty ('Succ n)] where
  TShiftCtx shift '[] = '[]
  TShiftCtx shift (ty ': tys) = (TShift 'Zero shift ty ': TShiftCtx tys)

type family TSubst (var :: Fin ('Succ n1))
                   (inner_ty :: Ty n1)
                   (outer_ty :: Ty ('Succ n1))
                   :: Ty n1 where
  TSubst var inner_ty ('TVar var) = inner_ty
  TSubst var inner_ty ('TVar var') = 'TVar (If (var <= var') (FPred var') (BumpFinDown var'))
  TSubst var inner_ty ('TForall ty) = 'TForall (TSubst ('FS var) (TShift 'Zero inner_ty) ty)
  TSubst var inner_ty (a ':~> b) = TSubst var inner_ty a ':~> TSubst var inner_ty b

data Expr :: [Ty n] -> Ty n -> * where
  Var :: Elem ctx ty -> Expr ctx ty
  Abs :: Expr (arg ': ctx) res -> Expr ctx (arg ':~> res)
  App :: Expr ctx (arg ':~> res) -> Expr ctx arg -> Expr ctx res
  TAbs :: Expr (TShiftCtx ('Succ 'Zero) ctx) ty -> Expr ctx ('TForall ty)
  TApp :: Expr ctx ('TForall res) -> STy arg -> Expr ctx (TSubst 'FZ arg res)

data Length :: [a] -> * where
  LZ :: Length '[]
  LS :: Length xs -> Length (x ': xs)

tshift :: Expr ctx ty -> Expr

shift :: forall ctx ty x. Expr ctx ty -> Expr (x ': ctx) ty
shift = go LZ
  where
    go :: forall ctx0 ty. Length ctx0
       -> Expr (ctx0 ++ ctx) ty -> Expr (ctx0 ++ x ': ctx) ty
    go ctx0 (Var v) = Var (shift_var ctx0 v)
    go ctx0 (Abs body) = Abs (go (LS ctx0) body)
    go ctx0 (App e1 e2) = App (go ctx0 e1) (go ctx0 e2)
    go ctx0 (TAbs body) = TAbs (_ (go ctx0 body))

    shift_var :: forall ctx0 ty. Length ctx0
              -> Elem (ctx0 ++ ctx) ty -> Elem (ctx0 ++ x ': ctx) ty
    shift_var LZ e = ES e
    shift_var (LS _) EZ = EZ
    shift_var (LS ctx0') (ES e') = ES (shift_var ctx0' e')
-}
goldfirere / ghc

Type-level GADT inference failure #29
