Substitution.hs

module TypeLet.Plugin.Substitution (
    letsToSubst
  , Cycle(..)
  , formatLetCycle
  ) where

import Data.Bifunctor
import Data.Foldable (toList)
import Data.List (intersperse)
import Data.List.NonEmpty (NonEmpty(..))
import Data.Maybe (mapMaybe)

import qualified Data.Graph as G

import TypeLet.Plugin.Constraints
import TypeLet.Plugin.GhcTcPluginAPI

-- | Construct idempotent substitution
--
-- TODO: Not entirely sure if this is correct, might be too simplistic and/or an
-- abuse of the ghc API; it is a /whole/ lot simpler than @niFixTCvSubst@, which
-- is disconcerning. However, it seems to work for the examples so far; perhaps
-- our use case is simpler? Needs more thought.
letsToSubst ::
     [GenLocated CtLoc CLet]
  -> Either (Cycle (GenLocated CtLoc CLet)) Subst
letsToSubst = fmap (uncurry zipTvSubst . unzip . go []) . inorder
  where
    go :: [(TyVar, Type)] -> [(TyVar, Type)] -> [(TyVar, Type)]
    go acc []         = acc
    go acc ((x, t):s) = go ((x, t) : map (second (subst1 x t)) acc) s

    subst1 :: TyVar -> Type -> Type -> Type
    subst1 x t = substTyWith [x] [t]

-- | Order the assignments
--
-- Suppose we have two assignments
--
-- > x := xT
-- > y := yT    where  x in (freevars yT)
--
-- Then the substitution should map @y@ to @(x := xT) yT@. We do this by
-- constructing the substitution in order, adding assignments one by one,
-- applying them to all assignments already in the accumulated substitution
-- as we go. In this example, this means adding @y := yT@ /first/, so that
-- we can apply @x := xT@ later (note that recursive definitions are
-- impossible in our use case).
--
-- In order to find the right order, we construct a graph of assignments. To
-- continue with our example, this graph will contain an edge
--
-- > (y := yT) -----> (x := xT)
--
-- The required assignment ordering is then obtained by topological sort.
inorder ::
     [GenLocated CtLoc CLet]
  -> Either (Cycle (GenLocated CtLoc CLet)) [(TyVar, Type)]
inorder lets =
    case cycles edges of
      c:_ -> Left c
      []  -> Right $ [
          (x, t)
        | (L _ (CLet _ x t), _, _) <- map nodeFromVertex $ G.topSort graph
        ]
  where
    graph          :: G.Graph
    nodeFromVertex :: G.Vertex -> (GenLocated CtLoc CLet, TyVar, [TyVar])
    _vertexFromKey :: TyVar -> Maybe G.Vertex
    (graph, nodeFromVertex, _vertexFromKey) = G.graphFromEdges edges

    edges :: [(GenLocated CtLoc CLet, TyVar, [TyVar])]
    edges = [
        ( l
        , y
        , [ x
          | L _ (CLet _ x _) <- lets
          , x `elemVarSet` (tyCoVarsOfType yT)
          ]
        )
      | l@(L _ (CLet _ y yT)) <- lets -- variables name match description above
      ]

-- | Format a cycle
--
-- We (arbitrarily) pick the first 'CLet' in the cycle for the location of the
-- error.
formatLetCycle ::
     Cycle (GenLocated CtLoc CLet)
  -> GenLocated CtLoc TcPluginErrorMessage
formatLetCycle (Cycle vs@(L l _ :| _)) = L l $
          Txt "Cycle in type-level let bindings: "
      :|: ( foldr1 (:|:)
          . intersperse (Txt ", ")
          . map (\(L _ l') -> formatCLet l')
          $ toList vs
          )

{-------------------------------------------------------------------------------
  Auxiliary
-------------------------------------------------------------------------------}

-- | Cycle in a graph
data Cycle a = Cycle (NonEmpty a)

cycles :: Ord key => [(node, key, [key])] -> [Cycle node]
cycles = mapMaybe aux . G.stronglyConnComp
  where
    aux :: G.SCC a -> Maybe (Cycle a)
    aux (G.AcyclicSCC _) = Nothing
    aux (G.CyclicSCC vs) =
        case vs of
          v:vs'      -> Just $ Cycle (v :| vs')
          _otherwise -> Nothing