Stack overflow!

[mrkgnao]

The problem is with inference for the last line, AFAICT: commenting it out makes reloads near-instant again.

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE InstanceSigs #-}

{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

{-# OPTIONS_GHC -fplugin=Coxswain #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=0 #-}

module Main where

import Data.Sculls.Symbol hiding ((.=))
import Data.Sculls.Internal.RecordAndVariant
import Data.Sculls.Internal.ShortVector
import Unsafe.Coerce
import qualified Data.Sculls.Symbol as Sculls
import GHC.TypeLits
import GHC.OverloadedLabels
import Control.Lens
import Data.Kind
import Data.Proxy
import GHC.Exts
import Control.Monad.Free
import Control.Monad (join)

(..=) = (Sculls..=)

data Wrap a l f = Functor f => Wrap (f a)
deriving instance Show (f a) => Show (Wrap a l f)

newtype Var rho a = Var (V (Wrap a) rho)

newtype Eff rho a = Eff (Free (Var rho) a)
  deriving stock   Functor
  deriving newtype Applicative
  deriving newtype Monad

instance Functor (Var r) where
  fmap :: forall a b r. (a -> b) -> Var r a -> Var r b
  fmap f (Var (MkV any w)) =
    case unsafeCoerce any of
      (Wrap v :: Wrap a l f) -> Var (MkV any' w)
        where any' = unsafeCoerce (Wrap (fmap f v) :: Wrap b l f)

newtype Reader r a = Reader { unReader :: r -> a }
  deriving stock Functor

run :: Monad m => (Var r (Eff r a) -> m (Eff r a)) -> Eff r a -> m a
run k = loop where loop = resume (\a -> k a >>= loop) pure

runReaderF
  :: forall (s :: Symbol) rho' rho r a p
   . ( Lacks rho' s
     , Lacks p "id"
     , rho' ~ Ext p "id" Identity
     , rho ~ Ext rho' s (Reader r)
     )
  => r
  -> Var rho (Eff rho a)
  -> Eff rho' (Eff rho a)
runReaderF r (Var v) = (Eff . liftF) =<< (Eff (Pure var))
 where
  var = case v .- (Proxy @s) of
    Left  l                  -> Var l
    Right (Wrap (Reader ra)) -> Var (mkV' (Wrap (pure (ra r))))
     where
      mkV'
        :: Wrap (Eff rho a) "id" Identity
        -> V (Wrap (Eff rho a)) (p .& "id" .= Identity)
      mkV' = mkV

instance Applicative (Reader r) where
  pure a = Reader (\_ -> a)
  rab <*> ra = Reader (\r -> unReader rab r (unReader ra r))

instance Monad (Reader r) where
  ra >>= arb = Reader (\r -> unReader (arb (unReader ra r)) r)

runReader = run runReaderF 

The error:

<λ> :l /home/mrkgnao/code/sans/sans/src/Main.hs
[1 of 1] Compiling Main             ( /home/mrkgnao/code/sans/sans/src/Main.hs, interpreted )
*** Exception: stack overflow

[mrkgnao]

It's a sensible function, however. This typechecks:

runReader
  :: forall (s :: Symbol) rho r a p
   . ( Lacks rho s
     , Lacks p "id"
     , rho ~ Ext p "id" Identity
     )
  => r 
  -> Eff (rho .& s .= (Reader r)) a
  -> Eff rho a
runReader r eff = run (runReaderF @s r) eff

Together with a runPure that extracts an a from an effect row with only the "id" .= Identity column and a couple ask-like primitives, we have

app :: Eff (Reading "reader" Int Base) Int
app = do
  s <- ask @"reader"
  pure (10 * s)

result :: Int
result = runPure (runReader @"reader" 2 app)

and GHCi says result is 20, as expected.

This is sort of a progress report, isn't it? :)

[nfrisby]

I'm away from my computer right now. Do you get a different behavior if you refactor a bit to avoid needing `-XAllowAmbiguousTypes`? (And maybe even `-XNoMonomorphismRestriction`?) Unrelated (I hope!): you might try using the `Data.Sculls.RAll` constraint instead of `Wrap`.

…

On Sun, Oct 22, 2017, 10:15 Soham Chowdhury ***@***.***> wrote: It's a sensible function, however: runReader :: forall (s :: Symbol) rho r a p . ( Lacks rho s , Lacks p "id" , rho ~ Ext p "id" Identity ) => r -> Eff (rho .& s .= (Reader r)) a -> Eff rho a runReader r eff = run (runReaderF @s r) eff — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#13 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABDg060Jea5GoJ39RG7_FQPi23JPRHBfks5su3g5gaJpZM4QCBWA> .

[mrkgnao]

An erratum to this comment: the version that triggered the stack overflow wasn't actually sensible and would never have typechecked.

Disabling AllowAmbiguousTypes would mean I'd have to pass around a proxy, like so:

runReaderF
  :: forall (s :: Symbol) rho' rho r a p proxy
   . ( Lacks rho' s
     , Lacks p "id"
     , rho' ~ Ext p "id" Identity
     , rho ~ Ext rho' s (Reader r)
     )
  => proxy s -> r
  -> Var rho  (Eff rho a)
  -> Eff rho' (Eff rho a)
runReaderF _ r (Var v) = (Eff . liftF) =<< (Eff (Pure var))
 where
  var = case v .- (Proxy @s) of
    Left  l                  -> Var l
    Right (Wrap (Reader ra)) -> Var (mkV' (Wrap (pure (ra r))))
     where
      mkV'
        :: Wrap (Eff rho a) "id" Identity
        -> V (Wrap (Eff rho a)) (p .& "id" .= Identity)
      mkV' = mkV

runReader = run (runReaderF (Proxy :: Proxy "reader"))

This triggers the same stack overflow. Additionally disabling NoMonomorphismRestriction makes typechecking, predictably, terminate quickly:

/home/mrkgnao/code/sans/sans/src/Main.hs:153:18: error:
    • Occurs check: cannot construct the infinite type:
        rho0
        ~
        (p0 .& ("id" .= Identity))
        .& ("reader"
            .= Reader
                 (Var
                    (p0 .& ("id" .= Identity))
                    (Eff (p0 .& ("id" .= Identity)) (Eff rho0 a0))))
        arising from a use of ‘runReaderF’
      The type variables ‘p0’, ‘a0’, ‘rho0’ are ambiguous
    • In the first argument of ‘run’, namely
        ‘(runReaderF (Proxy :: Proxy "reader"))’
      In the expression: run (runReaderF (Proxy :: Proxy "reader"))
      In an equation for ‘runReader’:
          runReader = run (runReaderF (Proxy :: Proxy "reader"))
    • Relevant bindings include
        runReader :: Eff (p0 .& ("id" .= Identity)) (Eff rho0 a0)
                     -> Var rho0 (Eff rho0 a0) -> Eff rho0 a0
          (bound at /home/mrkgnao/code/sans/sans/src/Main.hs:153:1)
    |
153 | runReader = run (runReaderF (Proxy :: Proxy "reader"))
    |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^