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

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

-- | Polymorphic length
module Morley.Prelude.Length
  ( length
  ) where

import Morley.Prelude.FromIntegral (CheckIntSubType, IntBaseType)

import Data.IntCast (IntBaseTypeK(..), IsIntSubType)
import GHC.TypeLits (ErrorMessage(..), TypeError)
import GHC.TypeNats (type (-))
import Universum hiding (length)
import Universum qualified

data Length

type instance IntBaseType Length = WordOfInt (IntBaseType Int)

type family WordOfInt ty where
  WordOfInt ('FixedIntTag n) = 'FixedWordTag (n - 1)
  WordOfInt ty = TypeError ('Text "Unexpected tag in WordOfInt: " ':<>: 'ShowType ty)

{- | Polymorphic version of 'Universum.length'.

Defaults to 'Int', same as the non-polymorphic version, if return value is
ambiguous.

>>> let list = [1..100]

>>> :t length list
length list :: Int

>>> length list :: Word
100
>>> length list :: Int
100
>>> length list :: Word63
100
>>> length list :: Natural
100
>>> length list :: Integer
100
>>> length list :: Word8
...
... error:
... Can not safely cast 'Morley.Prelude.Length.Length' to 'Word8':
... 'Morley.Prelude.Length.Length' is not a subtype of 'Word8'
...

One caveat that with an unsuitable monomorphic type, @length@ will also default
to 'Int':

>>> length list :: Bool
...
... error:
... Couldn't match type ‘Bool’ with ‘Int’
...

However, this lets us avoid the issue with integral literals.
-}
length
  :: (Integral i, Container a, DefaultToInt (IsIntSubType Length i) i)
  => a -> i
length = Universum.fromIntegral . Universum.length

type DefaultToInt :: Bool -> Type -> Constraint
class CheckIntSubType Length i => DefaultToInt b i

instance CheckIntSubType Length i => DefaultToInt 'True i
instance CheckIntSubType Length i => DefaultToInt 'False i

instance {-# incoherent #-} i ~ Int => DefaultToInt f i

{-
This incoherent instance trick merits a bit of an explanation. Basically, it
works like this: as long as @i@ is monomorphic and is a valid target type,
@IsIntSubType Length i@ is well-defined, that is, either @'True@ or @'False@,
thus non-incoherent instances get selected. If @i@ is polymorphic or an invalid
target type, then @IsIntSubType Length i@ is stuck, and the incoherent instance
can be selected, which will in turn force @i@ into @Int@.

-- @lierdakil
-}