{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE InstanceSigs        #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | The labelled telescope: a chain of binders, each carrying a label and a
-- payload in the scope before it.
--
-- This is the pattern behind a module's parameter block, a record signature,
-- or an algebraic theory: @(A : 𝕌) (m : A → A → A)@ is a two-step
-- telescope whose second payload mentions the first binder. Because a
-- telescope is a pattern ('CoSinkable', 'UnifiablePattern'), scope extension,
-- the names of a block, and α-equivalence of blocks come from the pattern
-- machinery, with the payloads compared through 'AlphaEquiv'.
--
-- What this module does not fix is what a payload /is/. The payload type is a
-- parameter, and the operations that need to look inside one, such as the
-- support a dependency closure needs, take the looking function as an
-- argument. A client instantiates the labels and payloads to its own types.
-- To close a declaration over the fields it uses, apply 'closeOverTelescope'
-- and then 'withThinnedNameBinderList'.
module Control.Monad.Foil.Telescope where

import           Control.Monad.Foil.Internal
import           Control.Monad.Foil.Relative (RelMonad, liftRM)

-- | A labelled telescope: a chain of binders, each carrying a label and a
-- payload in the scope before it.
--
-- The payload of a step lives in the scope the steps before it extend to, which
-- is what makes this a telescope rather than a list. For a module's parameters
-- the label is how the parameter is spelled and the payload is its type, so
-- that @(A : 𝕌) (m : A → A → A)@ is a two-step telescope whose second payload
-- mentions the first binder.
--
-- See 'NameBinderList', which this follows almost line for line.
--
-- @since 0.4.0
data Telescope label e n l where
  TelescopeEmpty :: Telescope label e n n
  TelescopeCons
    :: label                        -- ^ How the step is labelled.
    -> e n                          -- ^ Its payload, in the scope before it.
    -> NameBinder n i          -- ^ The binder it introduces.
    -> Telescope label e i l        -- ^ The steps after it.
    -> Telescope label e n l

-- | A telescope is a pattern, so the foil's own machinery walks it.
--
-- 'coSinkabilityProof' typechecks only because a payload is sunk by the
-- renaming of the scope /before/ its binder, rather than by the extended one.
--
-- 'withPattern' has to be written out rather than derived. The generic
-- implementation refuses a pattern with a field indexed by a scope, since it
-- would leave a payload that names a refreshed binder pointing at the name
-- that binder used to have. This instance follows the recipe in
-- 'transportPayload': a 'PatternTransport' threaded through the traversal,
-- with each payload moved by the transport accumulated /before/ its own
-- binder, that being the scope the payload lives in.
instance Sinkable e => CoSinkable (Telescope label e) where
  coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r.
(Name n -> Name n')
-> Telescope label e n l
-> (forall (l' :: S).
    (Name l -> Name l') -> Telescope label e n' l' -> r)
-> r
coSinkabilityProof Name n -> Name n'
rename Telescope label e n l
TelescopeEmpty forall (l' :: S).
(Name l -> Name l') -> Telescope label e n' l' -> r
cont = (Name l -> Name n') -> Telescope label e n' n' -> r
forall (l' :: S).
(Name l -> Name l') -> Telescope label e n' l' -> r
cont Name n -> Name n'
Name l -> Name n'
rename Telescope label e n' n'
forall label (e :: S -> *) (n :: S). Telescope label e n n
TelescopeEmpty
  coSinkabilityProof Name n -> Name n'
rename (TelescopeCons label
label e n
payload NameBinder n i
binder Telescope label e i l
rest) forall (l' :: S).
(Name l -> Name l') -> Telescope label e n' l' -> r
cont =
    (Name n -> Name n')
-> NameBinder n i
-> (forall (l' :: S). (Name i -> Name l') -> NameBinder n' l' -> r)
-> r
forall (n :: S) (n' :: S) (l :: S) r.
(Name n -> Name n')
-> NameBinder n l
-> (forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r)
-> r
forall (pattern :: S -> S -> *) (n :: S) (n' :: S) (l :: S) r.
CoSinkable pattern =>
(Name n -> Name n')
-> pattern n l
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)
-> r
coSinkabilityProof Name n -> Name n'
rename NameBinder n i
binder ((forall (l' :: S). (Name i -> Name l') -> NameBinder n' l' -> r)
 -> r)
-> (forall (l' :: S). (Name i -> Name l') -> NameBinder n' l' -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \Name i -> Name l'
rename' NameBinder n' l'
binder' ->
      (Name i -> Name l')
-> Telescope label e i l
-> (forall (l' :: S).
    (Name l -> Name l') -> Telescope label e l' l' -> r)
-> r
forall (n :: S) (n' :: S) (l :: S) r.
(Name n -> Name n')
-> Telescope label e n l
-> (forall (l' :: S).
    (Name l -> Name l') -> Telescope label e n' l' -> r)
-> r
forall (pattern :: S -> S -> *) (n :: S) (n' :: S) (l :: S) r.
CoSinkable pattern =>
(Name n -> Name n')
-> pattern n l
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)
-> r
coSinkabilityProof Name i -> Name l'
rename' Telescope label e i l
rest ((forall (l' :: S).
  (Name l -> Name l') -> Telescope label e l' l' -> r)
 -> r)
-> (forall (l' :: S).
    (Name l -> Name l') -> Telescope label e l' l' -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \Name l -> Name l'
rename'' Telescope label e l' l'
rest' ->
        (Name l -> Name l') -> Telescope label e n' l' -> r
forall (l' :: S).
(Name l -> Name l') -> Telescope label e n' l' -> r
cont Name l -> Name l'
rename''
          (label
-> e n'
-> NameBinder n' l'
-> Telescope label e l' l'
-> Telescope label e n' l'
forall label (e :: S -> *) (n :: S) (i :: S) (l :: S).
label
-> e n
-> NameBinder n i
-> Telescope label e i l
-> Telescope label e n l
TelescopeCons label
label ((Name n -> Name n') -> e n -> e n'
forall (n :: S) (l :: S). (Name n -> Name l) -> e n -> e l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
sinkabilityProof Name n -> Name n'
rename e n
payload) NameBinder n' l'
binder' Telescope label e l' l'
rest')

  withPattern
    :: forall f o n l r. Distinct o
    => (forall x y z r'. Distinct z
          => Scope z
          -> NameBinder x y
          -> (forall z'. DExt z z' => f x y z z' -> NameBinder z z' -> r')
          -> r')
    -> (forall x z z'. DExt z z' => f x x z z')
    -> (forall x y y' z z' z''. (DExt z z', DExt z' z'')
          => f x y z z' -> f y y' z' z'' -> f x y' z z'')
    -> Scope o
    -> Telescope label e n l
    -> (forall o'. DExt o o' => f n l o o' -> Telescope label e o o' -> Scope o' -> r)
    -> r
  withPattern :: forall (f :: S -> S -> S -> S -> *) (o :: S) (n :: S) (l :: S) r.
Distinct o =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> Telescope label e n l
-> (forall (o' :: S).
    DExt o o' =>
    f n l o o' -> Telescope label e o o' -> Scope o' -> r)
-> r
withPattern forall (x :: S) (y :: S) (z :: S) r'.
Distinct z =>
Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
withBinder forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z'
unit forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
f x y z z' -> f y y' z' z'' -> f x y' z z''
comp = PatternTransport n o
-> Scope o
-> Telescope label e n l
-> (forall (o' :: S).
    DExt o o' =>
    f n l o o' -> Telescope label e o o' -> Scope o' -> r)
-> r
forall (n' :: S) (l' :: S) (o' :: S) r'.
Distinct o' =>
PatternTransport n' o'
-> Scope o'
-> Telescope label e n' l'
-> (forall (o'' :: S).
    DExt o' o'' =>
    f n' l' o' o'' -> Telescope label e o' o'' -> Scope o'' -> r')
-> r'
go PatternTransport n o
forall (n :: S) (o :: S). PatternTransport n o
verbatimTransport
    where
      go :: forall n' l' o' r'. Distinct o'
         => PatternTransport n' o'
         -> Scope o'
         -> Telescope label e n' l'
         -> (forall o''. DExt o' o''
               => f n' l' o' o'' -> Telescope label e o' o'' -> Scope o'' -> r')
         -> r'
      go :: forall (n' :: S) (l' :: S) (o' :: S) r'.
Distinct o' =>
PatternTransport n' o'
-> Scope o'
-> Telescope label e n' l'
-> (forall (o'' :: S).
    DExt o' o'' =>
    f n' l' o' o'' -> Telescope label e o' o'' -> Scope o'' -> r')
-> r'
go PatternTransport n' o'
_transport Scope o'
scope Telescope label e n' l'
TelescopeEmpty forall (o'' :: S).
DExt o' o'' =>
f n' l' o' o'' -> Telescope label e o' o'' -> Scope o'' -> r'
cont = f n' l' o' o' -> Telescope label e o' o' -> Scope o' -> r'
forall (o'' :: S).
DExt o' o'' =>
f n' l' o' o'' -> Telescope label e o' o'' -> Scope o'' -> r'
cont f n' l' o' o'
f l' l' o' o'
forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z'
unit Telescope label e o' o'
forall label (e :: S -> *) (n :: S). Telescope label e n n
TelescopeEmpty Scope o'
scope
      go PatternTransport n' o'
transport Scope o'
scope (TelescopeCons label
label e n'
payload NameBinder n' i
binder Telescope label e i l'
rest) forall (o'' :: S).
DExt o' o'' =>
f n' l' o' o'' -> Telescope label e o' o'' -> Scope o'' -> r'
cont =
        Scope o'
-> NameBinder n' i
-> (forall (z' :: S).
    DExt o' z' =>
    f n' i o' z' -> NameBinder o' z' -> r')
-> r'
forall (x :: S) (y :: S) (z :: S) r'.
Distinct z =>
Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
withBinder Scope o'
scope NameBinder n' i
binder ((forall (z' :: S).
  DExt o' z' =>
  f n' i o' z' -> NameBinder o' z' -> r')
 -> r')
-> (forall (z' :: S).
    DExt o' z' =>
    f n' i o' z' -> NameBinder o' z' -> r')
-> r'
forall a b. (a -> b) -> a -> b
$ \f n' i o' z'
fbinder NameBinder o' z'
binder' ->
          PatternTransport i z'
-> Scope z'
-> Telescope label e i l'
-> (forall (o'' :: S).
    DExt z' o'' =>
    f i l' z' o'' -> Telescope label e z' o'' -> Scope o'' -> r')
-> r'
forall (n' :: S) (l' :: S) (o' :: S) r'.
Distinct o' =>
PatternTransport n' o'
-> Scope o'
-> Telescope label e n' l'
-> (forall (o'' :: S).
    DExt o' o'' =>
    f n' l' o' o'' -> Telescope label e o' o'' -> Scope o'' -> r')
-> r'
go (PatternTransport n' o'
-> NameBinder n' i -> NameBinder o' z' -> PatternTransport i z'
forall (n :: S) (o :: S) (i :: S) (o' :: S).
PatternTransport n o
-> NameBinder n i -> NameBinder o o' -> PatternTransport i o'
transportUnderBinder PatternTransport n' o'
transport NameBinder n' i
binder NameBinder o' z'
binder')
             (NameBinder o' z' -> Scope o' -> Scope z'
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
extendScope NameBinder o' z'
binder' Scope o'
scope)
             Telescope label e i l'
rest ((forall (o'' :: S).
  DExt z' o'' =>
  f i l' z' o'' -> Telescope label e z' o'' -> Scope o'' -> r')
 -> r')
-> (forall (o'' :: S).
    DExt z' o'' =>
    f i l' z' o'' -> Telescope label e z' o'' -> Scope o'' -> r')
-> r'
forall a b. (a -> b) -> a -> b
$ \f i l' z' o''
frest Telescope label e z' o''
rest' Scope o''
scope'' ->
            f n' l' o' o'' -> Telescope label e o' o'' -> Scope o'' -> r'
forall (o'' :: S).
DExt o' o'' =>
f n' l' o' o'' -> Telescope label e o' o'' -> Scope o'' -> r'
cont (f n' i o' z' -> f i l' z' o'' -> f n' l' o' o''
forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
f x y z z' -> f y y' z' z'' -> f x y' z z''
comp f n' i o' z'
fbinder f i l' z' o''
frest)
              (label
-> e o'
-> NameBinder o' z'
-> Telescope label e z' o''
-> Telescope label e o' o''
forall label (e :: S -> *) (n :: S) (i :: S) (l :: S).
label
-> e n
-> NameBinder n i
-> Telescope label e i l
-> Telescope label e n l
TelescopeCons label
label (PatternTransport n' o' -> e n' -> e o'
forall (e :: S -> *) (n :: S) (o :: S).
Sinkable e =>
PatternTransport n o -> e n -> e o
transportPayload PatternTransport n' o'
transport e n'
payload) NameBinder o' z'
binder' Telescope label e z' o''
rest')
              Scope o''
scope''

-- | Two telescopes unify when their binders line up and their payloads agree.
--
-- Labels are ignored, which is what α-equivalence should do with a label: a
-- parameter's spelling is no more relevant than a bound variable's. Payloads
-- are not, since two telescopes agreeing on binders may well disagree on types.
--
-- 'unifyPatterns' is the binder-only approximation, which is all a caller
-- without a scope can be given. 'unifyPatternsIn' is the real answer, and
-- it is what the library's α-equivalence calls.
instance (Sinkable e, AlphaEquiv e, RelMonad Name e)
    => UnifiablePattern (Telescope label e) where
  unifyPatterns :: forall (n :: S) (l :: S) (r :: S).
Distinct n =>
Telescope label e n l
-> Telescope label e n r
-> UnifyNameBinders (Telescope label e) n l r
unifyPatterns Telescope label e n l
TelescopeEmpty Telescope label e n r
TelescopeEmpty =
    NameBinders n l -> UnifyNameBinders (Telescope label e) n l l
forall (n :: S) (l :: S) (pattern :: S -> S -> *).
NameBinders n l -> UnifyNameBinders pattern n l l
SameNameBinders NameBinders n n
NameBinders n l
forall (n :: S). NameBinders n n
emptyNameBinders
  unifyPatterns (TelescopeCons label
_ e n
_ NameBinder n i
x Telescope label e i l
xs) (TelescopeCons label
_ e n
_ NameBinder n i
y Telescope label e i r
ys) =
    case (NameBinder n i -> DistinctEvidence i
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct NameBinder n i
x, NameBinder n i -> DistinctEvidence i
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct NameBinder n i
y) of
      (DistinctEvidence i
Distinct, DistinctEvidence i
Distinct) ->
        NameBinder n i
-> NameBinder n i -> UnifyNameBinders (Telescope label e) n i i
forall (i :: S) (l :: S) (r :: S) (pattern :: S -> S -> *).
Distinct i =>
NameBinder i l -> NameBinder i r -> UnifyNameBinders pattern i l r
unifyNameBinders NameBinder n i
x NameBinder n i
y UnifyNameBinders (Telescope label e) n i i
-> (Telescope label e i l, Telescope label e i r)
-> UnifyNameBinders (Telescope label e) n l r
forall (pattern :: S -> S -> *) (l :: S) (l' :: S) (n :: S)
       (r :: S) (r' :: S).
(UnifiablePattern pattern, Distinct l, Distinct l') =>
UnifyNameBinders pattern n l l'
-> (pattern l r, pattern l' r') -> UnifyNameBinders pattern n r r'
`andThenUnifyPatterns` (Telescope label e i l
xs, Telescope label e i r
ys)
  -- Telescopes of different lengths bind different numbers of names.
  unifyPatterns Telescope label e n l
_ Telescope label e n r
_ = UnifyNameBinders (Telescope label e) n l r
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (r :: S).
UnifyNameBinders pattern n l r
NotUnifiable

  unifyPatternsIn :: forall (n :: S) (l :: S) (r :: S).
Distinct n =>
Scope n
-> Telescope label e n l
-> Telescope label e n r
-> UnifyNameBinders (Telescope label e) n l r
unifyPatternsIn Scope n
scope Telescope label e n l
tele1 Telescope label e n r
tele2
    | Scope n
-> Telescope label e n l
-> Telescope label e n r
-> UnifyNameBinders (Telescope label e) n l r
-> Bool
forall label (e :: S -> *) (n :: S) (l :: S) (r :: S).
(Sinkable e, AlphaEquiv e, RelMonad Name e, Distinct n) =>
Scope n
-> Telescope label e n l
-> Telescope label e n r
-> UnifyNameBinders (Telescope label e) n l r
-> Bool
payloadsAgree Scope n
scope Telescope label e n l
tele1 Telescope label e n r
tele2 UnifyNameBinders (Telescope label e) n l r
verdict = UnifyNameBinders (Telescope label e) n l r
verdict
    | Bool
otherwise                               = UnifyNameBinders (Telescope label e) n l r
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (r :: S).
UnifyNameBinders pattern n l r
NotUnifiable
    where
      verdict :: UnifyNameBinders (Telescope label e) n l r
verdict = Telescope label e n l
-> Telescope label e n r
-> UnifyNameBinders (Telescope label e) n l r
forall (n :: S) (l :: S) (r :: S).
Distinct n =>
Telescope label e n l
-> Telescope label e n r
-> UnifyNameBinders (Telescope label e) n l r
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (r :: S).
(UnifiablePattern pattern, Distinct n) =>
pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
unifyPatterns Telescope label e n l
tele1 Telescope label e n r
tele2

-- | The payloads of a telescope, each moved into its innermost scope.
--
-- Sinking is free, so putting them all in one scope costs nothing and lets a
-- renaming be applied to the whole block at once.
--
-- @since 0.4.0
telescopePayloads
  :: (Sinkable e, Distinct l) => Telescope label e n l -> [e l]
telescopePayloads :: forall (e :: S -> *) (l :: S) label (n :: S).
(Sinkable e, Distinct l) =>
Telescope label e n l -> [e l]
telescopePayloads = (Param label e l -> e l) -> [Param label e l] -> [e l]
forall a b. (a -> b) -> [a] -> [b]
map Param label e l -> e l
forall label (e :: S -> *) (l :: S). Param label e l -> e l
paramType ([Param label e l] -> [e l])
-> (Telescope label e n l -> [Param label e l])
-> Telescope label e n l
-> [e l]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope label e n l -> [Param label e l]
forall (e :: S -> *) (l :: S) label (n :: S).
(Sinkable e, Distinct l) =>
Telescope label e n l -> [Param label e l]
telescopeParams

-- | Do the payloads of two telescopes agree, under the way their binders were
-- unified?
--
-- The verdict speaks about binders only, so the renaming it prescribes has to
-- be applied before the payloads are compared, which is exactly what
-- 'Control.Monad.Free.alphaEquivScoped' does to the body of a scoped term.
-- Comparing them as they stand would report @(A : 𝕌) (x : A)@ and
-- @(B : 𝕌) (y : B)@ as different, since the second payloads name different
-- binders until the first ones have been identified.
--
-- @since 0.4.0
payloadsAgree
  :: forall label e n l r.
     (Sinkable e, AlphaEquiv e, RelMonad Name e, Distinct n)
  => Scope n
  -> Telescope label e n l
  -> Telescope label e n r
  -> UnifyNameBinders (Telescope label e) n l r
  -> Bool
payloadsAgree :: forall label (e :: S -> *) (n :: S) (l :: S) (r :: S).
(Sinkable e, AlphaEquiv e, RelMonad Name e, Distinct n) =>
Scope n
-> Telescope label e n l
-> Telescope label e n r
-> UnifyNameBinders (Telescope label e) n l r
-> Bool
payloadsAgree Scope n
scope Telescope label e n l
tele1 Telescope label e n r
tele2 UnifyNameBinders (Telescope label e) n l r
verdict =
  case (Telescope label e n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct Telescope label e n l
tele1, Telescope label e n r -> DistinctEvidence r
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct Telescope label e n r
tele2) of
    (DistinctEvidence l
Distinct, DistinctEvidence r
Distinct) ->
      let payloads1 :: [e l]
payloads1 = Telescope label e n l -> [e l]
forall (e :: S -> *) (l :: S) label (n :: S).
(Sinkable e, Distinct l) =>
Telescope label e n l -> [e l]
telescopePayloads Telescope label e n l
tele1
          payloads2 :: [e r]
payloads2 = Telescope label e n r -> [e r]
forall (e :: S -> *) (l :: S) label (n :: S).
(Sinkable e, Distinct l) =>
Telescope label e n l -> [e l]
telescopePayloads Telescope label e n r
tele2
       in case UnifyNameBinders (Telescope label e) n l r
verdict of
            UnifyNameBinders (Telescope label e) n l r
NotUnifiable -> Bool
False
            -- The binders are the same, so the payloads already compare.
            SameNameBinders{} ->
              Scope l -> [e l] -> [e l] -> Bool
forall (m :: S). Distinct m => Scope m -> [e m] -> [e m] -> Bool
agree (Telescope label e n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern Telescope label e n l
tele1 Scope n
scope) [e l]
payloads1 [e l]
[e r]
payloads2
            -- The left telescope's binders become the right's, so its payloads
            -- have to follow them before they can be compared.
            RenameLeftNameBinder NameBinders n r
_ NameBinder n l -> NameBinder n r
renameL ->
              let scope' :: Scope r
scope' = Telescope label e n r -> Scope n -> Scope r
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern Telescope label e n r
tele2 Scope n
scope
               in Scope r -> [e r] -> [e r] -> Bool
forall (m :: S). Distinct m => Scope m -> [e m] -> [e m] -> Bool
agree Scope r
scope' ((e l -> e r) -> [e l] -> [e r]
forall a b. (a -> b) -> [a] -> [b]
map (Scope r -> (NameBinder n l -> NameBinder n r) -> e l -> e r
forall (i :: S) (m :: S).
Distinct m =>
Scope m -> (NameBinder n i -> NameBinder n m) -> e i -> e m
rename Scope r
scope' NameBinder n l -> NameBinder n r
renameL) [e l]
payloads1) [e r]
payloads2
            RenameRightNameBinder NameBinders n l
_ NameBinder n r -> NameBinder n l
renameR ->
              let scope' :: Scope l
scope' = Telescope label e n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern Telescope label e n l
tele1 Scope n
scope
               in Scope l -> [e l] -> [e l] -> Bool
forall (m :: S). Distinct m => Scope m -> [e m] -> [e m] -> Bool
agree Scope l
scope' [e l]
payloads1 ((e r -> e l) -> [e r] -> [e l]
forall a b. (a -> b) -> [a] -> [b]
map (Scope l -> (NameBinder n r -> NameBinder n l) -> e r -> e l
forall (i :: S) (m :: S).
Distinct m =>
Scope m -> (NameBinder n i -> NameBinder n m) -> e i -> e m
rename Scope l
scope' NameBinder n r -> NameBinder n l
renameR) [e r]
payloads2)
            -- Neither side's binders survive, so both blocks move to the
            -- unified ones.
            RenameBothBinders NameBinders n lr
binders NameBinder n l -> NameBinder n lr
renameL NameBinder n r -> NameBinder n lr
renameR ->
              case NameBinders n lr -> DistinctEvidence lr
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct NameBinders n lr
binders of
                DistinctEvidence lr
Distinct ->
                  let scope' :: Scope lr
scope' = NameBinders n lr -> Scope n -> Scope lr
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern NameBinders n lr
binders Scope n
scope
                   in Scope lr -> [e lr] -> [e lr] -> Bool
forall (m :: S). Distinct m => Scope m -> [e m] -> [e m] -> Bool
agree Scope lr
scope' ((e l -> e lr) -> [e l] -> [e lr]
forall a b. (a -> b) -> [a] -> [b]
map (Scope lr -> (NameBinder n l -> NameBinder n lr) -> e l -> e lr
forall (i :: S) (m :: S).
Distinct m =>
Scope m -> (NameBinder n i -> NameBinder n m) -> e i -> e m
rename Scope lr
scope' NameBinder n l -> NameBinder n lr
renameL) [e l]
payloads1)
                                   ((e r -> e lr) -> [e r] -> [e lr]
forall a b. (a -> b) -> [a] -> [b]
map (Scope lr -> (NameBinder n r -> NameBinder n lr) -> e r -> e lr
forall (i :: S) (m :: S).
Distinct m =>
Scope m -> (NameBinder n i -> NameBinder n m) -> e i -> e m
rename Scope lr
scope' NameBinder n r -> NameBinder n lr
renameR) [e r]
payloads2)
  where
    -- Lengths cannot disagree here: a verdict other than 'NotUnifiable'
    -- says the two telescopes bind the same number of names.
    agree :: forall m. Distinct m => Scope m -> [e m] -> [e m] -> Bool
    agree :: forall (m :: S). Distinct m => Scope m -> [e m] -> [e m] -> Bool
agree Scope m
scope' [e m]
xs [e m]
ys = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((e m -> e m -> Bool) -> [e m] -> [e m] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Scope m -> e m -> e m -> Bool
forall (n :: S). Distinct n => Scope n -> e n -> e n -> Bool
forall (e :: S -> *) (n :: S).
(AlphaEquiv e, Distinct n) =>
Scope n -> e n -> e n -> Bool
alphaEquivIn Scope m
scope') [e m]
xs [e m]
ys)

    rename
      :: forall i m. Distinct m
      => Scope m -> (NameBinder n i -> NameBinder n m) -> e i -> e m
    rename :: forall (i :: S) (m :: S).
Distinct m =>
Scope m -> (NameBinder n i -> NameBinder n m) -> e i -> e m
rename Scope m
scope' NameBinder n i -> NameBinder n m
f = Scope m -> (Name i -> Name m) -> e i -> e m
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
liftRM Scope m
scope' ((NameBinder n i -> NameBinder n m) -> Name i -> Name m
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
fromNameBinderRenaming NameBinder n i -> NameBinder n m
f)

-- | One step of a telescope, with everything about it moved into the innermost
-- scope.
--
-- Sinking is free, so this is the convenient form for anything that has to
-- compare parameters with the names of a term checked under all of them.
--
-- @since 0.4.0
data Param label e l = Param
  { forall label (e :: S -> *) (l :: S). Param label e l -> label
paramLabel :: label
  , forall label (e :: S -> *) (l :: S). Param label e l -> Name l
paramName  :: Name l
  , forall label (e :: S -> *) (l :: S). Param label e l -> e l
paramType  :: e l
  }

-- | The steps of a telescope, outermost first.
--
-- @since 0.4.0
telescopeParams
  :: (Sinkable e, Distinct l)
  => Telescope label e n l -> [Param label e l]
telescopeParams :: forall (e :: S -> *) (l :: S) label (n :: S).
(Sinkable e, Distinct l) =>
Telescope label e n l -> [Param label e l]
telescopeParams Telescope label e n l
TelescopeEmpty = []
telescopeParams (TelescopeCons label
label e n
ty NameBinder n i
binder Telescope label e i l
rest) =
  case (NameBinder n i -> ExtEvidence n i
forall (pattern :: S -> S -> *) (n :: S) (l :: S).
CoSinkable pattern =>
pattern n l -> ExtEvidence n l
assertExt NameBinder n i
binder, Telescope label e i l -> ExtEvidence i l
forall (pattern :: S -> S -> *) (n :: S) (l :: S).
CoSinkable pattern =>
pattern n l -> ExtEvidence n l
assertExt Telescope label e i l
rest) of
    (ExtEvidence n i
Ext, ExtEvidence i l
Ext) ->
      label -> Name l -> e l -> Param label e l
forall label (e :: S -> *) (l :: S).
label -> Name l -> e l -> Param label e l
Param label
label (Name i -> Name l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
sink (NameBinder n i -> Name i
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder n i
binder)) (e n -> e l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
sink e n
ty)
        Param label e l -> [Param label e l] -> [Param label e l]
forall a. a -> [a] -> [a]
: Telescope label e i l -> [Param label e l]
forall (e :: S -> *) (l :: S) label (n :: S).
(Sinkable e, Distinct l) =>
Telescope label e n l -> [Param label e l]
telescopeParams Telescope label e i l
rest

-- | The chain of binders a telescope forms.
--
-- This is 'nameBinderListOf' at a telescope, written out. The general one
-- goes through 'withPattern' and so rebuilds the telescope only to throw it
-- away, which is worth avoiding on the checking path.
--
-- @since 0.4.0
telescopeBinders :: Telescope label e n l -> NameBinderList n l
telescopeBinders :: forall label (e :: S -> *) (n :: S) (l :: S).
Telescope label e n l -> NameBinderList n l
telescopeBinders Telescope label e n l
TelescopeEmpty = NameBinderList n n
NameBinderList n l
forall (n :: S). NameBinderList n n
NameBinderListEmpty
telescopeBinders (TelescopeCons label
_ e n
_ NameBinder n i
binder Telescope label e i l
rest) =
  NameBinder n i -> NameBinderList i l -> NameBinderList n l
forall (n :: S) (i :: S) (l :: S).
NameBinder n i -> NameBinderList i l -> NameBinderList n l
NameBinderListCons NameBinder n i
binder (Telescope label e i l -> NameBinderList i l
forall label (e :: S -> *) (n :: S) (l :: S).
Telescope label e n l -> NameBinderList n l
telescopeBinders Telescope label e i l
rest)

-- | Close a set of parameters under the parameters their payloads need.
--
-- Keeping a parameter puts its payload into the result, so whatever that
-- payload mentions has to be kept too. A payload mentions only the parameters
-- before it, so working from the inside out settles it in one pass.
--
-- The support of a payload is the caller's to supply, since the library does
-- not know what a payload is. For terms of the free foil it is
-- 'Control.Monad.Free.Foil.supportOf'.
--
-- @since 0.4.0
closeOverTelescope
  :: Distinct l
  => (e l -> NameSet l)  -- ^ The support of a payload.
  -> [Param label e l] -> NameSet l -> NameSet l
closeOverTelescope :: forall (l :: S) (e :: S -> *) label.
Distinct l =>
(e l -> NameSet l) -> [Param label e l] -> NameSet l -> NameSet l
closeOverTelescope e l -> NameSet l
supportOfPayload [Param label e l]
params NameSet l
wanted = (Param label e l -> NameSet l -> NameSet l)
-> NameSet l -> [Param label e l] -> NameSet l
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Param label e l -> NameSet l -> NameSet l
close NameSet l
wanted [Param label e l]
params
  where
    close :: Param label e l -> NameSet l -> NameSet l
close Param label e l
p NameSet l
keep
      | Name l -> NameSet l -> Bool
forall (n :: S). Name n -> NameSet n -> Bool
nameSetMember (Param label e l -> Name l
forall label (e :: S -> *) (l :: S). Param label e l -> Name l
paramName Param label e l
p) NameSet l
keep = NameSet l
keep NameSet l -> NameSet l -> NameSet l
forall a. Semigroup a => a -> a -> a
<> e l -> NameSet l
supportOfPayload (Param label e l -> e l
forall label (e :: S -> *) (l :: S). Param label e l -> e l
paramType Param label e l
p)
      | Bool
otherwise                        = NameSet l
keep