{-

This test is inspired by
  Practical dependent type checking using twin types
  Victor López Juan and Nils Anders Danielsson
  TyDe '20
  https://dl.acm.org/doi/10.1145/3406089.3409030

The challenge is whether we can unify two types where the only
way to know that the kinds are equal is to unify the types. This
would fail in an algorithm that required kind unification before
type unification.
-}

{-# LANGUAGE TypeOperators, TypeApplications, DataKinds,
             StandaloneKindSignatures, PolyKinds, GADTs,
             TypeFamilies, NamedWildCards, PartialTypeSignatures #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}

module LopezJuan where

import Data.Type.Equality ( (:~~:)(..) )
import Data.Kind ( Type )
import Data.Proxy ( Proxy )

-- amazingly, this worked without modification

data SBool :: Bool -> Type where
  SFalse :: SBool False
  STrue  :: SBool True

data BoolOp where
  None :: Bool -> BoolOp
  Some :: Bool -> BoolOp

type F :: Bool -> Type
type family F b

get :: BoolOp -> Bool
get (None _) = True
get (Some x) = x

type Get :: BoolOp -> Bool
type family Get x where
  Get (None _) = True
  Get (Some x) = x

type TyFun :: Type -> Type -> Type
data TyFun arg res

type (~>) :: Type -> Type -> Type
type arg ~> res = TyFun arg res -> Type
infixr 0 ~>

data Const :: a -> (b ~> a)

f :: SBool x -> (:~~:) @(F (Get (_alpha x)) ~> BoolOp)
                       @(F True ~> BoolOp)
                       (Const (None x))
                       (Const (_alpha x))
f _ = HRefl

-- and something simpler:

type family Idish guard a where
  Idish True a = a
  Idish False a = Int

g :: (:~~:) @(Idish _alpha Type)
            @Type
            (Proxy _alpha)
            (Proxy True)
g = HRefl