{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}

module Constrained.TypeErrors (
  AssertComputes,
  module X,
) where

import Data.Kind
#if MIN_VERSION_base(4,17,0)
import GHC.TypeError as X
#else
import GHC.TypeLits as X
#endif

-- NOTE: this module implementes this very neat little trick for observing when type
-- families are stuck https://blog.csongor.co.uk/report-stuck-families/ which allows
-- us to report much better type errors when our generics tricks fail.
--
-- The idea of this type family is that if `ty` evaluates to a type (other than Dummy which
-- we haven't exported) then `Computes ty (TE err)` will evaluate to `()` without
-- getting stuck and without expanding `TE` to `TypeError err`.
--
-- If, on the other hand, GHC gets stuck evaluating `ty` it will (hopefully) try to normalize
-- everything and (hopefully) end up with `Computes (TypeError err) ty` which in turn will cause
-- it to throw `err` as a type error.
--
-- Now, the important thing here is that you can't do `Computes _ _ = ()` because that doesn't
-- force the evaluation of `ty` and consequently doesn't end up with GHC wanting to report
-- that `Computes tyThatDoesntCompute (TE err)` fails and consequently normalizing `TE err`
-- and finally arriving at `TypeError err`.
type family Computes (ty :: Type) (err :: Constraint) :: Constraint where
  Computes Dummy _ =
    TypeError
      (Text "This shouldn't be reachable because " :<>: ShowType Dummy :<>: Text " shouldn't be exported!")
  Computes _ _ = ()

-- This is intentionally hidden in here to avoid any funny business
data Dummy

-- NOTE: this indirection is necessary only for older versions of GHC where this is
-- "the right" amount of strictness - apparently it's not necessary on newer versions of GHC!
-- The alternative would be to just do `AssertComputes ty em = Computes ty (TypeError em)` below
-- and that works fine on e.g. ghc 9.12 (and other recent versions) but fails on 8.10.7 because
-- GHC is "too eager" to throw the type error.
type family TE em where
  TE em = TypeError em

type AssertComputes ty em = Computes ty (TE em)