open import Level
open import Data.List
open import Data.Nat
open import Data.Product
open import Data.Unit

module Normalise where

  private
    record Aggregate {ℓ} {t : Set ℓ} (_ : t) : Set (Level.suc ℓ) where
      field
        items : List (∃ λ (t' : Set ℓ) → t')

    open Aggregate

    unAggregateTypes : ∀ {ℓ} → List (∃ (λ (t' : Set ℓ) → t')) → _
    unAggregateTypes [] = Lift ⊤
    unAggregateTypes ((t , _) ∷ []) = t
    unAggregateTypes ((t , _) ∷ xs) = t × unAggregateTypes xs

    unAggregate : ∀ {ℓ} {t : Set ℓ} {x : t} → (c : Aggregate x) → unAggregateTypes (items c)
    unAggregate record { items = [] } = lift tt
    unAggregate record { items = items } = f items
      where
        f : (zs : _) → unAggregateTypes zs
        f [] = lift tt
        f ((_ , i) ∷ []) = i
        f ((_ , i) ∷ x ∷ xs) = i , f (x ∷ xs)

  instance
    ×-instance : ∀ {ℓ} {t₁ : Set ℓ} {t₂ : Set ℓ} {x : t₁} {y : t₂} {{_ : Aggregate x}} {{_ : Aggregate y}} → Aggregate (x , y)
    ×-instance {{i}} {{j}} = record { items = items i ++ items j }

  module add {ℓ} (t : Set ℓ) where
    instance
      i : ∀ {x : t} → Aggregate x
      i {x} = record { items = (_ , x) ∷ [] }


  refactor : ∀ {ℓ₁ ℓ₂} {t₁ : Set ℓ₁} {t₂ : Set ℓ₂} (x : t₁ × t₂) {{_ : Aggregate x}} → _
  refactor _ {{i}} = unAggregate i

open Normalise

-- example
mess : ((((⊤ × ℕ) × ℕ) × (ℕ × ⊤)) × (⊤ → ⊤))
mess = (((tt , ) , ) , ( , tt)) , λ x → x

clean : ⊤ × ℕ × ℕ × ℕ × ⊤ × (⊤ → ⊤)
clean = refactor mess
  where
    open add (⊤ → ⊤)
    open add ⊤
    open add ℕ

-- example 2
poly : ∀ {a b c d e : Set} → (((a × b × c) × d) × e) → a × b × c × d × e
poly {a} {b} {c} {d} {e} mess = refactor mess
  where
    open add a
    open add b
    open add c
    open add d
    open add e