{-# LANGUAGE LambdaCase, EmptyCase
           , EmptyDataDecls, TypeOperators, LiberalTypeSynonyms,
             ExistentialQuantification, GADTSyntax, GADTs

           , StandaloneDeriving

           , InstanceSigs, FlexibleContexts, MultiParamTypeClasses,
             FlexibleInstances , TypeSynonymInstances , FunctionalDependencies

           , TypeFamilies, TypeFamilyDependencies, DataKinds, PolyKinds,
             NoStarIsType , ConstraintKinds, QuantifiedConstraints , RankNTypes

           , ExplicitForAll, KindSignatures, ScopedTypeVariables,
             TypeApplications, ImplicitParams #-}

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UnicodeSyntax #-}

-- {-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module Implicit () where

import Data.Kind
import Data.Singletons.TH
import Data.Constraint

-- | Define the natural numbers recursively and do all the singletons/promotion
-- stuff to it:
$(singletons [d|
  data Nat :: Type where
    Z :: Nat
    S :: Nat -> Nat
  |])

-- | The family of the types of finite sets.
data Fin :: Nat -> Type where
  FZ :: Fin (S n)
  FS :: Fin n -> Fin (S n)
-- For whatever reason, `singletons` can't singletonize GADTs like `Fin`; in
-- case it's useful, see the bottom of this file for explicit implementations of
-- it.

data family (x :: a) !< (y :: a) :: Type
data instance (m :: Nat) !< (n :: Nat) where
  LTZ :: Z !< S n
  LTS :: m !< n -> S m !< S n

type family Super (c :: Constraint) :: Constraint

class Super (x &< y) => (x :: a) &< (y :: a) where
  lt_proof :: x !< y

type instance Super (Z &< S n) = ()
instance Z &< S n where
  lt_proof = LTZ

type instance Super (S m &< S n) = (m &< n)
instance m &< n => S m &< S n where
  lt_proof = LTS lt_proof

-- Doesn't work:
inj :: ∀ (m :: Nat) (n :: Nat). (m &< n) => SNat m -> SNat n -> Fin n
inj SZ      (SS _)  = FZ             -- Fine; the `Z &< S n` instance gets the job done
inj (SS n') (SS m') = FS (inj n' m') -- Everything breaks; the proof is uninferrable
-- We get:
{-
    • Could not deduce (n1 &< n2) arising from a use of ‘inj’
      from the context: m &< n
        bound by the type signature for:
                   inj :: forall (m :: Nat) (n :: Nat).
                          (m &< n) =>
                          SNat m -> SNat n -> Fin n
        at Implicit.hs:56:1-69
      or from: m ~ 'S n1
        bound by a pattern with constructor:
                   SS :: forall (n :: Nat). Sing n -> Sing ('S n),
                 in an equation for ‘inj’
        at Implicit.hs:58:6-10
      or from: n ~ 'S n2
        bound by a pattern with constructor:
                   SS :: forall (n :: Nat). Sing n -> Sing ('S n),
                 in an equation for ‘inj’
        at Implicit.hs:58:14-18
    • In the first argument of ‘FS’, namely ‘(inj n' m')’
      In the expression: FS (inj n' m')
      In an equation for ‘inj’: inj (SS n') (SS m') = FS (inj n' m')
   |
58 | inj (SS n') (SS m') = FS (inj n' m') -- Everything breaks; the proof is uninferrable
   |                           ^^^^^^^^^
-}

_LTD'' ∷ S m !< S n → m !< n
_LTD'' (LTS lt) = lt

-- I think this is the real heart of the problem?
_LTD' ∷ Dict (S m &< S n) → Dict (m &< n)
_LTD' Dict = undefined

-- But how would you even use this?
_LTD ∷ (S m &< S n) :- (m &< n)
_LTD = unmapDict _LTD'

--------------------------------------------------------------------------------
-- In case it's useful, here are singleton types and whatnot for `Fin`. (For
-- reasons I don't understand, `singletons` can't automatically generate these
-- for GADTs like `Fin`. Since everything below works, I guess `singletons`
-- usually does more than this, and it's one or more of those other things that
-- aren't possible.)

data instance Sing (_fn :: Fin n) where
  SFZ :: Sing FZ
  SFS :: Sing fn -> Sing (FS fn)

type SFin = (Sing :: Fin n -> Type)

instance SingI FZ where
  sing = SFZ

instance SingI fn => SingI (FS fn) where
  sing = SFS (sing :: Sing fn)

instance SingKind (Fin n) where
  type instance Demote (Fin n) = Fin n
  fromSing SFZ = FZ
  fromSing (SFS n) = FS (fromSing n)
  toSing FZ = SomeSing SFZ
  toSing (FS n) = case toSing n of
    SomeSing sfn -> SomeSing (SFS sfn)