-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Instructions working on sum types derived from Haskell ones.
module Morley.Michelson.Typed.Haskell.Instr.Sum
  ( InstrWrapC
  , InstrWrapOneC
  , InstrCaseC
  , InstrUnwrapC
  , instrWrap
  , instrWrapOne
  , hsWrap
  , instrCase
  , (//->)
  , unsafeInstrUnwrap
  , hsUnwrap

  , CaseClauseParam (..)
  , CaseClause (..)
  , CaseClauses
  , GCaseClauses
  , GCaseBranchInput

  , Branch (..)
  , Path
  , CtorField (..)
  , ExtractCtorField
  , AppendCtorField
  , AppendCtorFieldAxiom
  , appendCtorFieldAxiom
  , GetCtorField
  , CtorHasOnlyField
  , CtorOnlyField
  , MyCompoundType

    -- * Helpers
  , IsPrimitiveValue
  ) where

import Data.Constraint (Bottom(..))
import Data.Singletons (SingI(..))
import Data.Type.Bool (type (||))
import Data.Vinyl.Core (Rec(..))
import GHC.Generics ((:*:)(..), (:+:)(..))
import GHC.Generics qualified as G
import GHC.TypeLits (AppendSymbol, ErrorMessage(..), Symbol, TypeError)
import Type.Reflection ((:~:)(Refl))
import Unsafe.Coerce (unsafeCoerce)

import Morley.Michelson.Text (MText, mt)
import Morley.Michelson.Typed.Entrypoints
import Morley.Michelson.Typed.Haskell.Instr.Helpers
import Morley.Michelson.Typed.Haskell.Value
import Morley.Michelson.Typed.Instr
import Morley.Michelson.Typed.T
import Morley.Michelson.Typed.Value
import Morley.Tezos.Address (Address)
import Morley.Tezos.Core (ChainId, Mutez, Timestamp)
import Morley.Tezos.Crypto (KeyHash, PublicKey, Signature)
import Morley.Util.Generic
import Morley.Util.Label (Label)
import Morley.Util.Named
import Morley.Util.Type
import Morley.Util.TypeTuple

{- $setup
>>> import Morley.Util.Named
>>> import Morley.Michelson.Typed
>>> import Fmt (pretty)
-}

-- Constructors lookup (helper)
----------------------------------------------------------------------------

-- | We support only two scenarious - constructor with one field and
-- without fields. Nonetheless, it's not that sad since for sum types
-- we can't even assign names to fields if there are many (the style
-- guide prohibits partial records).
data CtorField
  = OneField Type
  | NoFields

-- | Get /something/ as field of the given constructor.
type family ExtractCtorField (cf :: CtorField) where
  ExtractCtorField ('OneField t) = t
  ExtractCtorField 'NoFields = ()

-- | Push field to stack, if any.
type AppendCtorField :: CtorField -> [k] -> [k]
type family AppendCtorField cf l where
  AppendCtorField ('OneField t) (l :: [T]) = ToT t ': l
  AppendCtorField ('OneField t) (l :: [Type]) = t ': l
  AppendCtorField 'NoFields (l :: [T]) = l
  AppendCtorField 'NoFields (l :: [Type]) = l

-- | To use 'AppendCtorField' not only here for 'T'-based stacks, but also
-- later in Lorentz with 'Type'-based stacks we need the following property.
type AppendCtorFieldAxiom (cf :: CtorField) (st :: [Type]) =
  ToTs (AppendCtorField cf st) ~ AppendCtorField cf (ToTs st)

-- | Proof of 'AppendCtorFieldAxiom'.
appendCtorFieldAxiom
  :: ( AppendCtorFieldAxiom ('OneField Word) '[Int]
     , AppendCtorFieldAxiom 'NoFields '[Int]
     )
  => Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom =
  -- In order to avoid a lot of boilerplate and burdening GHC type checker we
  -- write an unsafe code. Its correctness is tested in dummy constraints of
  -- this function.
  -- Alternative approach I compare this unsafe one with
  -- would be to implement @instance SingI@ for 'CtorField' and consider cases
  -- of 'CtorField' one by one, but this would require propagading
  -- @SingI (cf :: CtorField)@ constraint to all users of 'appendCtorFieldAxiom'.
  unsafeCoerce $ Dict @(AppendCtorFieldAxiom 'NoFields '[])

-- | Result of constructor lookup - entry type and path to it in the tree.
data LookupNamedResult = LNR CtorField Path

type family LnrFieldType (lnr :: LookupNamedResult) where
  LnrFieldType ('LNR f _) = f
type family LnrBranch (lnr :: LookupNamedResult) :: Path where
  LnrBranch ('LNR _ p) = p

-- | Transitively find constructor of some sum type by its name.
--
-- Transitivity means that if sum type consists of other sum types,
-- they will be searched recursively.
type GetNamed name a = LNRequireFound name a (GLookupNamed name (GRep a))

-- | Force result of 'GLookupNamed' to be 'Just'
type family LNRequireFound
  (name :: Symbol)
  (a :: Type)
  (mf :: Maybe LookupNamedResult)
    :: LookupNamedResult where
  LNRequireFound _ _ ('Just lnr) = lnr
  LNRequireFound name a 'Nothing = TypeError
    ('Text "Datatype " ':<>: 'ShowType a ':<>:
     'Text " has no (sub)constructor " ':<>: 'ShowType name)

type family GLookupNamed (name :: Symbol) (x :: Type -> Type)
          :: Maybe LookupNamedResult where
  GLookupNamed name (G.D1 _ x) = GLookupNamed name x
  GLookupNamed name (G.C1 ('G.MetaCons ctorName _ _) x) =
    -- This case corresponds to going straight into a data type (as
    -- opposed to going left or right when we encounter a sum type),
    -- so we need to prepend 'S' here if we successfully find a
    -- constructor.
    PrependS
    -- If we encounter a constructor with requested name, we consider
    -- search successful.
    (If (name == ctorName || name == ("c" `AppendSymbol` ctorName))
       ('Just $ 'LNR (GExtractFields x) '[])
        -- If we do not, we check whether we can go deeper (see
        -- description below).
        (If (GCanGoDeeper x)
        -- And here we essentially just recursively call this search.
        (GLookupNamedDeeper name x)
        -- Or return 'Nothing' if we can not go deeper.
         'Nothing
      )
    )
  GLookupNamed name (x :+: y) =
    LNMergeFound name (GLookupNamed name x) (GLookupNamed name y)
  GLookupNamed _ G.V1 = 'Nothing

-- Prepend 'S' to the path inside 'LookupNamedResult' (if 'Just' is passed).
-- Should be done in the case when we go straight into a data type.
type family PrependS (x :: Maybe LookupNamedResult) :: Maybe LookupNamedResult where
  PrependS 'Nothing = 'Nothing
  PrependS ('Just ('LNR cf path)) = 'Just ('LNR cf ('S ': path))

-- Helper type family to check whether we should search for a
-- constructor inside given data type which is supposed to be part of
-- another constructor. Basically we can go deeper only if we
-- encounter another ADT with a constructor storing at least something
-- and which is not a primitive type. We do not go deeper when we
-- encounter a product type here, because it means that there are multiple
-- fields inside one constructor (it is not supported).
type family GCanGoDeeper (x :: Type -> Type) :: Bool where
  GCanGoDeeper (_ :+: _) = 'True
  GCanGoDeeper (G.D1 _ x) = GCanGoDeeper x
  GCanGoDeeper (G.S1 _ (G.Rec0 x)) = CanGoDeeper x
  GCanGoDeeper (G.C1 _ _) = 'True
  GCanGoDeeper G.V1 = 'False
  GCanGoDeeper G.U1 = 'False
  GCanGoDeeper (_ :*: _) = 'False
  GCanGoDeeper x = TypeError
    ('Text "GCanGoDeeper encountered unexpected pattern: " ':<>: 'ShowType x)

-- | Whether given type represents an atomic Michelson value.
type family IsPrimitiveValue (x :: Type) :: Bool where
  IsPrimitiveValue (Maybe _) = 'True
  IsPrimitiveValue (NamedF _ _ _) = 'True
  IsPrimitiveValue Integer = 'True
  IsPrimitiveValue Natural = 'True
  IsPrimitiveValue Text = 'True
  IsPrimitiveValue MText = 'True
  IsPrimitiveValue Bool = 'True
  IsPrimitiveValue ByteString = 'True
  IsPrimitiveValue Mutez = 'True
  IsPrimitiveValue Address = 'True
  IsPrimitiveValue EpAddress = 'True
  IsPrimitiveValue KeyHash = 'True
  IsPrimitiveValue Timestamp = 'True
  IsPrimitiveValue PublicKey = 'True
  IsPrimitiveValue Signature = 'True
  IsPrimitiveValue (ContractRef _) = 'True
  IsPrimitiveValue (BigMap _ _) = 'True
  IsPrimitiveValue (Map _ _) = 'True
  IsPrimitiveValue (Set _) = 'True
  IsPrimitiveValue ([_]) = 'True
  IsPrimitiveValue (Operation' _) = 'True
  IsPrimitiveValue ChainId = 'True
  IsPrimitiveValue _ = 'False

-- Some types don't have Generic instances (e. g. primitives like Integer), so
-- we need another type family to handle them.
type CanGoDeeper (x :: Type) =
  If (IsPrimitiveValue x)
     'False
     (GCanGoDeeper (GRep x))

type family GLookupNamedDeeper (name :: Symbol) (x :: Type -> Type)
          :: Maybe LookupNamedResult where
  GLookupNamedDeeper name (G.S1 _ (G.Rec0 y))  = GLookupNamed name (GRep y)
  GLookupNamedDeeper name _ = TypeError
    ('Text "Attempt to go deeper failed while looking for sum type constructor"
     ':<>: 'ShowType name
     ':$$:
     'Text "Make sure that all constructors have exactly one field inside."
    )

type family LNMergeFound
  (name :: Symbol)
  (f1 :: Maybe LookupNamedResult)
  (f2 :: Maybe LookupNamedResult)
    :: Maybe LookupNamedResult where
  LNMergeFound _ 'Nothing 'Nothing = 'Nothing
  LNMergeFound _ ('Just ('LNR a p)) 'Nothing = 'Just $ 'LNR a ('L ': p)
  LNMergeFound _ 'Nothing ('Just ('LNR a p)) = 'Just $ 'LNR a ('R ': p)
  LNMergeFound name ('Just _) ('Just _) = TypeError
    ('Text "Ambiguous reference to datatype constructor: " ':<>: 'ShowType name)

type family GExtractFields (x :: Type -> Type)
          :: CtorField where
  GExtractFields (G.S1 _ x) = GExtractFields x
  GExtractFields (G.Rec0 a) = 'OneField a
  GExtractFields G.U1 = 'NoFields
  GExtractFields (_ :*: _) = TypeError
    ('Text "Cannot automatically lookup constructors having multiple fields"
     ':$$:
     'Text "Consider using tuple instead")
    --- ^ @martoon: Probably we will have no use cases for such scenario
    --- anyway, tuples seem to be not worse than separate fields in most cases.

{- | Get type of constructor fields (one or zero) referred by given datatype and
name.

>>> data Foo = Foo1 Bool | Foo2 ()
>>> () :: CtorOnlyField "Foo2" Foo
...
... GHC.Generics.Rep Foo
... is stuck. Likely
... Generic Foo
... instance is missing or out of scope.
...

>>> data Foo = Foo1 Bool | Foo2 () deriving Generic
>>> :kind! GetCtorField Foo "Foo2"
...
= 'OneField ()
-}
type GetCtorField dt ctor =
  LnrFieldType (GetNamed ctor dt)

-- | Expect referred constructor to have only one field (in form of constraint)
-- and extract its type.
type CtorHasOnlyField ctor dt f =
  GetCtorField dt ctor ~ 'OneField f

type family RequireOneField (ctor :: Symbol) (cf :: CtorField) :: Type where
  RequireOneField _ ('OneField f) = f
  RequireOneField ctor 'NoFields = TypeError
    ('Text "Expected exactly one field" ':$$:
     'Text "In constructor " ':<>: 'ShowType ctor)

-- | Expect referred constructor to have only one field
-- (otherwise compile error is raised) and extract its type.
type CtorOnlyField name dt =
  RequireOneField name (GetCtorField dt name)

----------------------------------------------------------------------------
-- Constructor wrapping instruction
----------------------------------------------------------------------------

{- | Wrap given element into a constructor with the given name.

Mentioned constructor must have only one field.

Since labels interpretable by @OverloadedLabels@ extension cannot start with
capital latter, prepend constructor name with letter "c" (see examples below).

>>> data Foo = FooCtor () | FooCtor2 Bool
>>> instrWrap @Foo #cFooCtor
...
... GHC.Generics.Rep Foo
... is stuck. Likely
... Generic Foo
... instance is missing or out of scope.
...

>>> data Foo = FooCtor | FooCtor2 Bool deriving (Generic, IsoValue)
>>> pretty $ instrWrap @Foo #cFooCtor2
[RIGHT unit]
>>> pretty $ instrWrap @Foo #cFooCtor
[PUSH unit Unit, LEFT bool]
-}
instrWrap
  :: forall dt name st.
     InstrWrapC dt name
  => Label name
  -> Instr (AppendCtorField (GetCtorField dt name) st)
           (ToT dt ': st)
instrWrap _ =
  gInstrWrap @(GRep dt) @(LnrBranch (GetNamed name dt))
                         @(LnrFieldType (GetNamed name dt))

{- | Like 'instrWrap' but only works for contructors with a single field.
Results in a type error if a constructor with no field is used instead.

>>> data Foo = FooCtor | FooCtor2 Bool
>>> instrWrapOne @Foo #cFooCtor
...
... GHC.Generics.Rep Foo
... is stuck. Likely
... Generic Foo
... instance is missing or out of scope.
...

>>> data Foo = FooCtor | FooCtor2 Bool deriving (Generic, IsoValue)
>>> pretty $ instrWrapOne @Foo #cFooCtor2
[RIGHT unit]
>>> pretty $ instrWrapOne @Foo #cFooCtor
...
... Expected exactly one field
... In constructor "cFooCtor"
...
-}
instrWrapOne
  :: forall dt name st.
     InstrWrapOneC dt name
  => Label name
  -> Instr (ToT (CtorOnlyField name dt) ': st) (ToT dt ': st)
instrWrapOne _ =
  gInstrWrap @(GRep dt) @(LnrBranch (GetNamed name dt))
                         @(LnrFieldType (GetNamed name dt))

type InstrWrapC dt name =
  ( GenericIsoValue dt
  , GInstrWrap (GRep dt)
      (LnrBranch (GetNamed name dt))
      (LnrFieldType (GetNamed name dt))
  )

type InstrWrapOneC dt name =
  ( InstrWrapC dt name
  , GetCtorField dt name ~ 'OneField (CtorOnlyField name dt)
  )

-- | Wrap a haskell value into a constructor with the given name.
--
-- This is symmetric to 'instrWrap'.
hsWrap
  :: forall dt name.
     InstrWrapC dt name
  => Label name
  -> ExtractCtorField (GetCtorField dt name)
  -> dt
hsWrap _ =
  G.to . gHsWrap @(GRep dt) @(LnrBranch (GetNamed name dt))
                             @(LnrFieldType (GetNamed name dt))

-- | Generic traversal for 'instrWrap'.
class
  GInstrWrap
    (x :: Type -> Type)
    (path :: Path)
    (entryTy :: CtorField) where
  gInstrWrap
    :: Instr (AppendCtorField entryTy s) (GValueType x ': s)
  gHsWrap
    :: ExtractCtorField entryTy -> x p

instance GInstrWrap x path e => GInstrWrap (G.D1 i x) path e where
  gInstrWrap = gInstrWrap @x @path @e
  gHsWrap = G.M1 . gHsWrap @x @path @e

instance (GInstrWrap x path e, SingI (GValueType y)) =>
         GInstrWrap (x :+: y) ('L ': path) e where
  gInstrWrap = gInstrWrap @x @path @e `Seq` LEFT
  gHsWrap = G.L1 . gHsWrap @x @path @e

instance (GInstrWrap y path e, SingI (GValueType x)) =>
         GInstrWrap (x :+: y) ('R ': path) e where
  gInstrWrap = gInstrWrap @y @path @e `Seq` RIGHT
  gHsWrap = G.R1 . gHsWrap @y @path @e

instance GInstrWrap (G.C1 c (G.S1 i (G.Rec0 e))) '[ 'S] ('OneField e) where
  gInstrWrap = Nop
  gHsWrap = G.M1 . G.M1 . G.K1

-- This is the case when a sum type is part of another sum type.
-- Here 'sub' is intermediate sum type.
instance ( path ~ (x ': xs)
         , GInstrWrap (GRep sub) path e
         , GenericIsoValue sub
         ) =>
         GInstrWrap (G.C1 c (G.S1 i (G.Rec0 sub))) ('S ': x ': xs) e where
  gInstrWrap = gInstrWrap @(GRep sub) @path @e
  gHsWrap = G.M1 . G.M1 . G.K1 . G.to . gHsWrap @(GRep sub) @path @e

instance GInstrWrap (G.C1 c G.U1) '[ 'S] 'NoFields where
  gInstrWrap = PUSH VUnit
  gHsWrap () = G.M1 G.U1

-- Examples
----------------------------------------------------------------------------

-- TODO [TM-186]: Consider moving this stuff to test-suite using
-- doctest. Or at least add tests for correctness.

data MyType
  = MyCtor Integer
  | ComplexThing ()
  | UselessThing ("field1" :! ByteString, "field2" :! ())
  deriving stock Generic
  deriving anyclass IsoValue

_MyTypeMyCtor ::
  GetNamed "cMyCtor" MyType :~: 'LNR ('OneField Integer) '[ 'L, 'S]
_MyTypeMyCtor = Refl

_MyTypeComplexThing ::
  GetNamed "cComplexThing" MyType :~: 'LNR ('OneField ()) '[ 'R, 'L, 'S]
_MyTypeComplexThing = Refl

_wrapMyType1 :: Instr (ToT Integer ': s) (ToT MyType ': s)
_wrapMyType1 = instrWrap @MyType #cMyCtor

-- If @c@ prefix is too annoying, one can construct labels without
-- @OverloadedLabels@ extension.
_wrapMyType1' :: Instr (ToT Integer ': s) (ToT MyType ': s)
_wrapMyType1' = instrWrap @MyType @"MyCtor" fromLabel

_wrapMyType2 :: Instr (ToT () ': s) (ToT MyType ': s)
_wrapMyType2 = instrWrap @MyType #cComplexThing

_wrapMyType3 :: Instr (ToT (ByteString, ()) ': s) (ToT MyType ': s)
_wrapMyType3 = instrWrap @MyType #cUselessThing

data MyType' = WrapBool Bool
  deriving stock Generic
  deriving anyclass IsoValue

_MyType'WrapBool ::
  GetNamed "cWrapBool" MyType' :~: 'LNR ('OneField Bool) '[ 'S]
_MyType'WrapBool = Refl

_wrapMyType' :: Instr (ToT Bool ': s) (ToT MyType' ': s)
_wrapMyType' = instrWrap @MyType' #cWrapBool

data MyCompoundType
  = CompoundPart1 MyType
  | CompoundPart2 Integer
  | CompoundPart3 Address
  | CompoundPart4 MyType'
  deriving stock Generic
  deriving anyclass IsoValue

_MyCompoundTypeCompoundPart1 ::
  GetNamed "cCompoundPart1" MyCompoundType :~: 'LNR ('OneField MyType) '[ 'L, 'L, 'S]
_MyCompoundTypeCompoundPart1 = Refl

_MyCompoundTypeMyCtor ::
  GetNamed "cMyCtor" MyCompoundType :~: 'LNR ('OneField Integer) '[ 'L, 'L, 'S, 'L, 'S]
_MyCompoundTypeMyCtor = Refl

_MyCompoundTypeCompoundPart2 ::
  GetNamed "cCompoundPart2" MyCompoundType :~: 'LNR ('OneField Integer) '[ 'L, 'R, 'S]
_MyCompoundTypeCompoundPart2 = Refl

_MyCompoundTypeCompoundPart4 ::
  GetNamed "cCompoundPart4" MyCompoundType :~: 'LNR ('OneField MyType') '[ 'R, 'R, 'S]
_MyCompoundTypeCompoundPart4 = Refl

_MyCompoundTypeWrapBool ::
  GetNamed "cWrapBool" MyCompoundType :~: 'LNR ('OneField Bool) '[ 'R, 'R, 'S, 'S]
_MyCompoundTypeWrapBool = Refl

_wrapMyCompoundType1 :: Instr (ToT Integer ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType1 = instrWrap @MyCompoundType #cMyCtor

_wrapMyCompoundType2 :: Instr (ToT Integer ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType2 = instrWrap @MyCompoundType #cCompoundPart2

_wrapMyCompoundType3 :: Instr (ToT Bool ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType3 = instrWrap @MyCompoundType #cWrapBool

_wrapMyCompoundType4 :: Instr (ToT MyType' ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType4 = instrWrap @MyCompoundType #cCompoundPart4

data MyEnum = Case1 | Case2 | CaseN Integer | CaseDef
  deriving stock Generic
  deriving anyclass IsoValue

_wrapMyEnum1 :: Instr s (ToT MyEnum ': s)
_wrapMyEnum1 = instrWrap @MyEnum #cCase1

_wrapMyEnum2 :: Instr (ToT Integer ': s) (ToT MyEnum ': s)
_wrapMyEnum2 = instrWrap @MyEnum #cCaseN

data MyTypeWithNamedField
  = MeaninglessCtor
  | CtorWithNamedField ("name" :! Natural)
  deriving stock Generic
  deriving anyclass IsoValue

_accessMyTypeWithNamedField :: Instr (ToT Natural ': s) (ToT MyTypeWithNamedField ': s)
_accessMyTypeWithNamedField = instrWrap @MyTypeWithNamedField #cCtorWithNamedField

----------------------------------------------------------------------------
-- "case" instruction
----------------------------------------------------------------------------

-- | Pattern-match on the given datatype.
instrCase
  :: forall dt out inp.
     InstrCaseC dt
  => Rec (CaseClause inp out) (CaseClauses dt) -> RemFail Instr (ToT dt ': inp) out
instrCase = fst . gInstrCase @(GRep dt) @'[]

type InstrCaseC dt = (GenericIsoValue dt, GInstrCase (GRep dt) '[])

-- | In what different case branches differ - related constructor name and
-- input stack type which the branch starts with.
data CaseClauseParam = CaseClauseParam Symbol CtorField

-- | Type information about single case clause.
data CaseClause (inp :: [T]) (out :: [T]) (param :: CaseClauseParam) where
  CaseClause
    :: RemFail Instr (AppendCtorField x inp) out
    -> CaseClause inp out ('CaseClauseParam ctor x)

-- | Lift an instruction to case clause.
--
-- You should write out constructor name corresponding to the clause
-- explicitly. Prefix constructor name with "c" letter, otherwise
-- your label will not be recognized by Haskell parser.
-- Passing constructor name can be circumvented but doing so is not recomended
-- as mentioning contructor name improves readability and allows avoiding
-- some mistakes.
(//->)
  :: Label ("c" `AppendSymbol` ctor)
  -> RemFail Instr (AppendCtorField x inp) out
  -> CaseClause inp out ('CaseClauseParam ctor x)
(//->) _ = CaseClause
infixr 8 //->

-- | List of 'CaseClauseParam's required to pattern match on the given type.
type CaseClauses a = GCaseClauses (GRep a) '[]


-- | Generic traversal for 'instrWrap'.
class GInstrCase (x :: Type -> Type) (rest :: [CaseClauseParam]) where
  type GCaseClauses x rest :: [CaseClauseParam]

  gInstrCase
    :: forall inp out.
       Rec (CaseClause inp out) (GCaseClauses x rest)
    -> (RemFail Instr (GValueType x ': inp) out, Rec (CaseClause inp out) rest)

instance GInstrCase x rest => GInstrCase (G.D1 i x) rest where
  type GCaseClauses (G.D1 i x) rest = GCaseClauses x rest
  gInstrCase = gInstrCase @x @rest

instance (GInstrCase x (GCaseClauses y rest), GInstrCase y rest) =>
         GInstrCase (x :+: y) rest where
  type GCaseClauses (x :+: y) rest = GCaseClauses x (GCaseClauses y rest)
  gInstrCase clauses
    | (lres, rest) <- gInstrCase @x clauses
    , (rres, rest') <- gInstrCase @y rest
    = (rfMerge IF_LEFT lres rres, rest')

instance GInstrCase G.V1 rest where
  type GCaseClauses G.V1 rest = rest
  gInstrCase rest = (RfAlwaysFails NEVER, rest)

instance GInstrCaseBranch ctor x => GInstrCase (G.C1 ('G.MetaCons ctor _1 _2) x) rest where
  type GCaseClauses (G.C1 ('G.MetaCons ctor _1 _2) x) rest = GCaseBranchInput ctor x ': rest
  gInstrCase (clause :& rest) = (gInstrCaseBranch @ctor @x clause, rest)

-- | Traverse a single contructor and supply its field to instruction in case clause.
class GInstrCaseBranch (ctor :: Symbol) (x :: Type -> Type) where

  type GCaseBranchInput ctor x :: CaseClauseParam

  gInstrCaseBranch
    :: CaseClause inp out (GCaseBranchInput ctor x)
    -> RemFail Instr (GValueType x ': inp) out

instance
  ( TypeError ('Text "Cannot pattern match on constructors with more than 1 field"
               ':$$: 'Text "Consider using tuples instead")
  , Bottom
  ) => GInstrCaseBranch ctor (x :*: y) where
  type GCaseBranchInput ctor (x :*: y) = 'CaseClauseParam ctor 'NoFields
  gInstrCaseBranch = no

instance GInstrCaseBranch ctor x => GInstrCaseBranch ctor (G.S1 i x) where
  type GCaseBranchInput ctor (G.S1 i x) = GCaseBranchInput ctor x
  gInstrCaseBranch = gInstrCaseBranch @ctor @x

instance GInstrCaseBranch ctor (G.Rec0 a) where
  type GCaseBranchInput ctor (G.Rec0 a) = 'CaseClauseParam ctor ('OneField a)
  gInstrCaseBranch (CaseClause i) = i

instance GInstrCaseBranch ctor G.U1 where
  type GCaseBranchInput ctor G.U1 = 'CaseClauseParam ctor 'NoFields
  gInstrCaseBranch (CaseClause i) = rfMapAnyInstr (DROP `Seq`) i

-- Examples
----------------------------------------------------------------------------

_caseMyType :: RemFail Instr (ToT MyType ': s) (ToT Integer ': s)
_caseMyType = instrCase @MyType $
     #cMyCtor //-> RfNormal Nop
  :& #cComplexThing //-> RfNormal (DROP `Seq` PUSH (toVal @Integer 5))
  :& #cUselessThing //-> RfNormal (DROP `Seq` PUSH (toVal @Integer 0))
  :& RNil

-- Another version, written via tuple.
_caseMyType2 :: RemFail Instr (ToT MyType ': s) (ToT Integer ': s)
_caseMyType2 = instrCase @MyType $ recFromTuple
  ( #cMyCtor //->
      RfNormal Nop
  , #cComplexThing //->
      RfNormal (DROP `Seq` PUSH (toVal @Integer 5))
  , #cUselessThing //->
      RfNormal (DROP `Seq` PUSH (toVal @Integer 0))
  )

_caseMyEnum :: RemFail Instr (ToT MyEnum ': ToT Integer ': s) (ToT Integer ': s)
_caseMyEnum = instrCase @MyEnum $ recFromTuple
  ( #cCase1 //-> RfNormal (DROP `Seq` PUSH (toVal @Integer 1))
  , #cCase2 //-> RfNormal (DROP `Seq` PUSH (toVal @Integer 2))
  , #cCaseN //-> RfNormal (DIP DROP `Seq` Nop)
  , #cCaseDef //-> RfNormal Nop
  )

----------------------------------------------------------------------------
-- Constructor unwrapping instruction
----------------------------------------------------------------------------

-- | Unwrap a constructor with the given name.
--
-- Rules which apply to 'instrWrap' function work here as well.
-- Although, unlike @instrWrap@, this function does not work for nullary
-- constructors.
unsafeInstrUnwrap
  :: forall dt name st.
     InstrUnwrapC dt name
  => Label name
  -> Instr (ToT dt ': st)
           (ToT (CtorOnlyField name dt) ': st)
unsafeInstrUnwrap _ =
  unsafeGInstrUnwrap @(GRep dt) @(LnrBranch (GetNamed name dt))
                                 @(CtorOnlyField name dt)

type InstrUnwrapC dt name =
  ( GenericIsoValue dt
  , GInstrUnwrap (GRep dt)
      (LnrBranch (GetNamed name dt))
      (CtorOnlyField name dt)
  )

-- | Try to unwrap a constructor with the given name.
hsUnwrap
  :: forall dt name.
     InstrUnwrapC dt name
  => Label name
  -> dt
  -> Maybe (CtorOnlyField name dt)
hsUnwrap _ =
  gHsUnwrap @(GRep dt) @(LnrBranch (GetNamed name dt))
            @(CtorOnlyField name dt) .
  G.from

class GInstrUnwrap
    (x :: Type -> Type)
    (path :: Path)
    (entryTy :: Type) where
  unsafeGInstrUnwrap
    :: Instr (GValueType x ': s) (ToT entryTy ': s)
  gHsUnwrap
    :: x p -> Maybe entryTy

instance GInstrUnwrap x path e => GInstrUnwrap (G.D1 i x) path e where
  unsafeGInstrUnwrap = unsafeGInstrUnwrap @x @path @e
  gHsUnwrap = gHsUnwrap @x @path @e . G.unM1

instance (GInstrUnwrap x path e, SingI (GValueType y)) =>
         GInstrUnwrap (x :+: y) ('L ': path) e where
  unsafeGInstrUnwrap = IF_LEFT (unsafeGInstrUnwrap @x @path @e) failWithWrongCtor
  gHsUnwrap = \case
    G.L1 x -> gHsUnwrap @x @path @e x
    G.R1 _ -> Nothing

instance (GInstrUnwrap y path e, SingI (GValueType x)) =>
         GInstrUnwrap (x :+: y) ('R ': path) e where
  unsafeGInstrUnwrap = IF_LEFT failWithWrongCtor (unsafeGInstrUnwrap @y @path @e)
  gHsUnwrap = \case
    G.R1 y -> gHsUnwrap @y @path @e y
    G.L1 _ -> Nothing

instance (IsoValue e) =>
         GInstrUnwrap (G.C1 c (G.S1 i (G.Rec0 e))) '[ 'S] e where
  unsafeGInstrUnwrap = Nop
  gHsUnwrap = Just . G.unK1 . G.unM1 . G.unM1

-- This is the case when a sum type is part of another sum type.
-- Here 'sub' is intermediate sum type.
instance ( path ~ (x ': xs)
         , GInstrUnwrap (GRep sub) path e
         , GenericIsoValue sub
         ) =>
         GInstrUnwrap (G.C1 c (G.S1 i (G.Rec0 sub))) ('S ': x ': xs) e where
  unsafeGInstrUnwrap = unsafeGInstrUnwrap @(GRep sub) @path @e
  gHsUnwrap = gHsUnwrap @(GRep sub) @path @e . G.from . G.unK1 . G.unM1 . G.unM1

-- | Failure indicating that we expected value created with one constructor,
-- but got value with different one.
-- The error message is intentionally ugly to keep it relatively short and
-- save on gas.
failWithWrongCtor :: Instr i o
failWithWrongCtor =
  PUSH (toVal [mt|BadCtor|]) `Seq`
  FAILWITH

-- Examples
----------------------------------------------------------------------------

_unwrapMyType :: Instr (ToT MyType ': s) (ToT Integer ': s)
_unwrapMyType = unsafeInstrUnwrap @MyType #cMyCtor

_unwrapMyCompoundType :: Instr (ToT MyCompoundType ': s) (ToT Integer ': s)
_unwrapMyCompoundType = unsafeInstrUnwrap @MyCompoundType #cMyCtor

_unwrapMyCompoundType2 :: Instr (ToT MyCompoundType ': s) (ToT Address ': s)
_unwrapMyCompoundType2 = unsafeInstrUnwrap @MyCompoundType #cCompoundPart3

_unwrapMyCompoundType3 :: Instr (ToT MyCompoundType ': s) (ToT Bool ': s)
_unwrapMyCompoundType3 = unsafeInstrUnwrap @MyCompoundType #cWrapBool

_unwrapMyCompoundType4 :: Instr (ToT MyCompoundType ': s) (ToT MyType' ': s)
_unwrapMyCompoundType4 = unsafeInstrUnwrap @MyCompoundType #cCompoundPart4