An attempt at a well-typed implementation of Complete+Easy. Needless to say, it does not work.

Bidir.idr

module Bidir

Ident : Type
Ident = String

mutual
  BaseCtx' : Type
  Ctx' : BaseCtx' -> Type
  CtxItem' : (b : BaseCtx') -> (c : Ctx' b) -> Type

  Nil' : Ctx' b
  Snoc' : (c : Ctx' b) -> CtxItem' b c -> Ctx' b

  BaseNil' : BaseCtx'
  BaseSnoc' : (b : BaseCtx') -> CtxItem' b (Nil' {b=b}) -> BaseCtx'

  IsUVar' : Ident -> (b : BaseCtx') -> Ctx' b -> Type
  IsEVar' : Ident -> (b : BaseCtx') -> Ctx' b -> Type

  VarType' : (b : BaseCtx') -> (c : Ctx' b) -> Type

  CtxUVar' : Ident -> CtxItem' b c
  CtxEVar' : Ident -> Maybe (VarType' b c) -> CtxItem' b c

  data CtxItem : (b : BaseCtx') -> (c : Ctx' b) -> Type where
    CtxUVar : Ident -> CtxItem b c
    CtxEVar : Ident -> Maybe (VarType' b c) -> CtxItem b c

  ||| Universal variables.  These are implicitly universally quantified over.
  data UVar : (b : BaseCtx') -> (c : Ctx' b) -> Type where
    MkUVar : (name : Ident) -> IsUVar' name b c -> UVar b c
  ||| Existential variables.  These (hopefully) all get solved for specific types.
  data EVar : (b : BaseCtx') -> (c : Ctx' b) -> Type where
    MkEVar : (name : Ident) -> IsEVar' name b c -> EVar b c

  ||| The type of terms in the language
  data VarType : (b : BaseCtx') -> (c : Ctx' b) -> Type where
    TUnit : VarType b c
    TUVar : UVar b c -> VarType b c
    TEVar : EVar b c -> VarType b c
    TArrow : VarType b c -> VarType b c -> VarType b c
    TForall : (name : Ident)
      -> VarType b (Snoc' {b=b} c (CtxUVar' {b=b} {c=c} name))
      -> VarType b c

  data BaseCtx : Type where
    BaseNil : BaseCtx
    BaseSnoc : (ctx : BaseCtx') -> (i : CtxItem ctx (Nil' {b = ctx})) -> BaseCtx

  data Ctx : BaseCtx' -> Type where
    Nil : Ctx b
    Snoc : (x : Ctx' b) -> CtxItem b x -> Ctx b

  namespace UVar
    public export
    data IsUVar : (name : Ident) -> (b : BaseCtx') -> (c : Ctx' b) -> Type where
      BaseHere : IsUVar name (BaseSnoc' b (CtxUVar' {b=b} {c=(Nil' {b=b})} name))
                    (Nil' {b=(BaseSnoc' b (CtxUVar' {b=b} {c=(Nil' {b=b})} name))})
      BaseThere : IsUVar name b (Nil' {b=b})
        -> IsUVar name (BaseSnoc' b i)
              (Nil' {b=(BaseSnoc' b i)})
      Here : IsUVar name b (Snoc' {b=b} c (CtxUVar' {b=b} {c=c} name))
      There : IsUVar name b c -> IsUVar name b (Snoc' {b=b} c i)
  namespace EVar
    public export
    data IsEVar : (name : Ident) -> (b : BaseCtx') -> (c : Ctx' b) -> Type where
      BaseHere : IsEVar name (BaseSnoc' b (CtxEVar' {b=b} {c=(Nil' {b=b})} name ty))
                    (Nil' {b=(BaseSnoc' b (CtxEVar' {b=b} {c=(Nil' {b=b})} name ty))})
      BaseThere : IsEVar name b (Nil' {b=b})
        -> IsEVar name (BaseSnoc' b i)
              (Nil' {b=(BaseSnoc' b i)})
      Here : IsEVar name b (Snoc' {b=b} c (CtxEVar' {b=b} {c=c} name ty))
      There : IsEVar name b c -> IsEVar name b (Snoc' {b=b} c i)

  BaseCtx' = BaseCtx
  BaseNil' = BaseNil
  Ctx' = Ctx
  Nil' = Nil
  CtxItem' = CtxItem
  BaseSnoc' = BaseSnoc
  Snoc' = Snoc
  IsUVar' = IsUVar
  IsEVar' = IsEVar
  VarType' = VarType
  CtxUVar' = CtxUVar
  CtxEVar' = CtxEVar

mutual
  namespace BaseCtx
    public export
    (++) : (b : BaseCtx) -> (y : Ctx b) -> BaseCtx
  namespace Ctx
    public export
    (++) : {0 b : BaseCtx} -> (xs : Ctx b) -> (ys : Ctx (b ++ xs)) -> Ctx b

  appendNilId : {b : BaseCtx} -> (c : Ctx b) -> c ++ Nil = c

  namespace BaseCtx
    b ++ Nil = b
    b ++ (Snoc ys y) = (b ++ ys) `BaseSnoc` rebase {ty=CtxItem} b ys Nil (rewrite appendNilId ys in y)
  namespace Ctx
    xs ++ Nil = xs
    xs ++ (Snoc ys y) = (xs ++ ys) `Snoc` unrebase _ _ _ y

  appendNilId c = Refl

  weakenCtx : (0 b : BaseCtx)
    -> (ys : Ctx b)
    -> (xs : Ctx b)
    -> Ctx (b ++ ys)
  weakenCtx b ys Nil = Nil
  weakenCtx b ys (Snoc xs x) with (weaken b xs ys Nil x)
  weakenCtx b ys (Snoc xs x) | x' with (weakenCtx b ys xs)
  weakenCtx b ys (Snoc xs x) | x' | rec = rec `Snoc` rebase _ _ _ x'

  interface Rebase (ty : (b : BaseCtx) -> Ctx b -> Type) where
    rebase : (0 b : BaseCtx)
      -> (0 xs : Ctx b)
      -> (  ys : Ctx (b ++ xs))
      -> ty b (xs ++ ys) -> ty (b ++ xs) ys
    unrebase : (0 b : BaseCtx)
      -> (0 xs : Ctx b)
      -> (  ys : Ctx (b ++ xs))
      -> ty (b ++ xs) ys -> ty b (xs ++ ys)
    weaken : (0 b : BaseCtx)
      -> (0 xs : Ctx b)
      -> (  ys : Ctx b)
      -> (  zs : Ctx (b ++ (ys ++ weakenCtx b ys xs)))
      -> ty b xs -> ty b ((ys ++ weakenCtx b ys xs) ++ zs)

  Rebase CtxItem where
    rebase b xs ys (CtxUVar name) = CtxUVar name
    rebase b xs ys (CtxEVar name ty) = CtxEVar name $ map (rebase b xs ys) ty
    unrebase b xs ys (CtxUVar name) = CtxUVar name
    unrebase b xs ys (CtxEVar name ty) = CtxEVar name $ map (unrebase b xs ys) ty
    weaken b xs ys zs (CtxUVar x) = CtxUVar x
    weaken b xs ys zs (CtxEVar x y) = CtxEVar x $ map (weaken b xs ys zs) y

  Rebase (IsUVar n) where
    rebase (BaseSnoc b (CtxUVar n)) Nil Nil BaseHere = BaseHere
    rebase (BaseSnoc b i) Nil Nil (BaseThere x) = BaseThere x
    rebase b (Snoc c (CtxUVar n)) Nil Here = BaseHere
    rebase b (Snoc c i) Nil (There x)
      = BaseThere $ rebase _ _ _ x
    rebase b xs (Snoc ys (CtxUVar n)) Here = Here
    rebase b xs (Snoc ys y) (There x) = There $ rebase _ _ _ x

    unrebase b xs (Snoc ys (CtxUVar n)) Here = Here
    unrebase b xs (Snoc ys y) (There x) = There $ unrebase _ _ _ x
    unrebase b xs Nil Here impossible

    weaken (BaseSnoc b (CtxUVar n)) Nil Nil Nil BaseHere = BaseHere
    weaken (BaseSnoc b (CtxUVar n)) Nil (Snoc ys y) Nil BaseHere = There $ weaken _ Nil ys Nil BaseHere
    weaken (BaseSnoc b i) Nil Nil Nil (BaseThere x) = BaseThere x
    weaken (BaseSnoc b i) Nil (Snoc ys y) Nil (BaseThere x) = There $ weaken _ Nil ys Nil (BaseThere x)
    weaken b (Snoc xs (CtxUVar n)) ys Nil Here = Here
    weaken b (Snoc xs i) ys Nil (There x) = There $ weaken b xs ys Nil x
    weaken b xs ys (Snoc zs z) x = There $ weaken _ _ _ _ x

  Rebase (IsEVar n) where
    rebase (BaseSnoc b (CtxEVar n ty)) Nil Nil BaseHere = BaseHere
    rebase (BaseSnoc b i) Nil Nil (BaseThere x) = BaseThere x
    rebase b (Snoc c (CtxEVar n ty)) Nil Here = BaseHere
    rebase b (Snoc c i) Nil (There x)
      = BaseThere $ rebase _ _ _ x
    rebase b xs (Snoc ys (CtxEVar n ty)) Here = Here
    rebase b xs (Snoc ys y) (There x) = There $ rebase _ _ _ x

    unrebase b xs (Snoc ys (CtxEVar n ty)) Here = Here
    unrebase b xs (Snoc ys y) (There x) = There $ unrebase _ _ _ x
    unrebase b xs Nil Here impossible

    weaken (BaseSnoc b (CtxEVar n ty)) Nil Nil Nil BaseHere = BaseHere
    weaken (BaseSnoc b (CtxEVar n ty)) Nil (Snoc ys y) Nil BaseHere = There $ weaken _ Nil ys Nil BaseHere
    weaken (BaseSnoc b i) Nil Nil Nil (BaseThere x) = BaseThere x
    weaken (BaseSnoc b i) Nil (Snoc ys y) Nil (BaseThere x) = There $ weaken _ Nil ys Nil (BaseThere x)
    weaken b (Snoc xs (CtxEVar n ty)) ys Nil Here = Here
    weaken b (Snoc xs i) ys Nil (There x) = There $ weaken b xs ys Nil x
    weaken b xs ys (Snoc zs z) x = There $ weaken _ _ _ _ x

  Rebase UVar where
    rebase b xs ys (MkUVar name x) = MkUVar name $ rebase _ _ _ x
    unrebase b xs ys (MkUVar name x) = MkUVar name $ unrebase _ _ _ x
    weaken b xs ys zs (MkUVar name x) = MkUVar name $ weaken _ _ _ _ x

  Rebase EVar where
    rebase b xs ys (MkEVar name x) = MkEVar name $ rebase _ _ _ x
    unrebase b xs ys (MkEVar name x) = MkEVar name $ unrebase _ _ _ x
    weaken b xs ys zs (MkEVar name x) = MkEVar name $ weaken _ _ _ _ x

  Rebase VarType where
    rebase b xs ys TUnit = TUnit
    rebase b xs ys (TUVar v) = TUVar $ rebase _ _ _ v
    rebase b xs ys (TEVar v) = TEVar $ rebase _ _ _ v
    rebase b xs ys (TArrow x y) = TArrow (rebase _ _ _ x) (rebase _ _ _ y)
    rebase b xs ys (TForall name x) = TForall name $ rebase _ _ _ x
    unrebase b xs ys TUnit = TUnit
    unrebase b xs ys (TUVar x) = TUVar $ unrebase _ _ _ x
    unrebase b xs ys (TEVar x) = TEVar $ unrebase _ _ _ x
    unrebase b xs ys (TArrow x y) = TArrow (unrebase _ _ _ x) (unrebase _ _ _ y)
    unrebase b xs ys (TForall name x) = TForall name $ unrebase _ _ _ x
    weaken b xs ys zs TUnit = TUnit
    weaken b xs ys zs (TUVar x) = TUVar $ weaken _ _ _ _ x
    weaken b xs ys zs (TEVar x) = TEVar $ weaken _ _ _ _ x
    weaken b xs ys zs (TArrow x y) = TArrow (weaken _ _ _ _ x) (weaken _ _ _ _ y)
    weaken b xs ys zs (TForall name x) = TForall name $ ?weaken_hole

-------------- proofs ---------------
snocInj : Snoc xs x = Snoc ys y -> xs = ys
snocInj Refl = Refl

mutual
  interface Rebase ty => LegitRebase (ty : (b : BaseCtx) -> Ctx b -> Type) where
    rebaseUnrebase : (b : BaseCtx)
      -> (xs : Ctx b)
      -> (ys : Ctx (b ++ xs))
      -> (eq : b ++ (xs ++ ys) = (b ++ xs) ++ ys)
      -> (i : ty (b ++ xs) ys)
      -> i = rebase b xs ys (unrebase b xs ys i)

  LegitRebase CtxItem where
    rebaseUnrebase b xs ys eq (CtxUVar name) = Refl
    rebaseUnrebase b xs ys eq (CtxEVar name Nothing) = Refl

    -- *** This gives a really weird error message when you use that definition
    -- 
    -- Bidir.idr:232:58--232:85:While processing right hand side of rebaseUnrebase at Bidir.idr:232:5--234:3:
    -- Can't solve constraint between:
    --     rebase b xs ys (unrebase b xs ys ty)
    -- and
    --     rebase b xs ys (unrebase b xs ys ty)
    -- at:
    -- 232         rebaseUnrebase b xs ys eq (CtxEVar name (Just ty)) = cong (CtxEVar name . Just) $ rebaseUnrebase b xs ys eq ty
    --                                                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^
    rebaseUnrebase b xs ys eq (CtxEVar name (Just ty)) = ?hole1 -- cong (CtxEVar name . Just) $ rebaseUnrebase b xs ys eq ty

  LegitRebase (IsUVar n) where
    rebaseUnrebase b xs Nil eq Here impossible
    rebaseUnrebase b xs (Snoc ys (CtxUVar n)) eq Here = Refl

    -- *** This line gives the empty error message -- not sure at all what it means
    rebaseUnrebase b xs (Snoc ys i) eq (There x) with (rebaseUnrebase b xs ys (snocInj eq) x)
    rebaseUnrebase b xs (Snoc ys i) eq (There x) | ind = ?hole

  LegitRebase (IsEVar n) where
    rebaseUnrebase b xs ys eq x = ?hole2

  LegitRebase UVar where
    rebaseUnrebase b xs ys eq x = ?hole3

  LegitRebase EVar where
    rebaseUnrebase b xs ys eq x = ?hole4

  LegitRebase VarType where
    rebaseUnrebase b xs ys eq x = ?hole5