nfrisby / coxswain Goto Github PK

View Code? Open in Web Editor NEW

39.0 39.0 1.0 90 KB

A GHC type checker plugin for row types

License: BSD 3-Clause "New" or "Revised" License

Haskell 99.86% Awk 0.14%

coxswain's People

Stargazers

Watchers

Forkers

galtys

coxswain's Issues

Resolve the Col var story

I defined the .& and .= families separately so that we could have the rather natural syntax that we have.

But doing it this way opens the possibility of type variables inhabiting the Col kind, when I really don't think those will ever be interesting. For now, I've asked the user (in Haddock) to avoid such Col vars.

But the plugin code still has some old attempts at worrying about this. I think it's basically dead code. (E.G. Some of it implements injectivity of the .= family; but I think the type family dependencies now make that redundant.)

This task is to decide on how best to handle Col vars and to then prune/simplify that code in the plugin.

Add `Lacks` constraint to `HasSomeCol`

In vproof, the tag of MkV should be used as that Lacks constraint's evidence.

Cannot show mkR

Nice work, but I had some surprises while experimenting with the plugin interactively (with GHC 8.2.1). Here's one:

$ ghci -fplugin=Coxswain -XOverloadedLabels -XDataKinds -XTypeFamilies -XTypeOperators -XFlexibleContexts -fconstraint-solver-iterations=1000
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Prelude> :m + Data.Sculls.Symbol
Prelude Data.Sculls.Symbol> mkR

<interactive>:1:1: error:
    solveSimpleWanteds: too many iterations (limit = 1000)
      Set limit with -fconstraint-solver-iterations=n; n=0 for no limit
      Simples = {[WD] $dShow_a5oB {0}:: Show a0 (CNonCanonical),
                 [WD] hole{a5oD} {0}:: R f0 Row0 ~ a0 (CNonCanonical)}
      WC = WC {wc_simple =
                 [WD] $dShort_a74z {0}:: Short (0 GHC.TypeNats.- 1) (CNonCanonical)
                 [WD] $dCoxswainWorking_a627 {0}:: Coxswain.CoxswainWorking
                                                     0 (CDictCan)}

Stack overflow!

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

Is `handsoff` necessary?

The handsoff pass prevents row unification from articulating an untouchable variable. At first blush, that seems right.

However, because of the Ren-based approach, articulation is a "pure" operation: its has no effect outside of the scope of the givens that incurred it. So does touchableness matter?

GHC internal error: stg_ap_p_ret

This looks like a bad coercion somewhere.

runReader
  :: forall (s :: Symbol) (bs :: Symbol) base rho r a p
   . (Lacks rho s, Lacks p bs, rho ~ Ext p bs base, Applicative base)
  => r
  -> Eff (Ext rho s (Reader r)) a
  -> Eff rho a
runReader r eff = run (runReaderF @s @bs @base r) eff

app :: Eff (Reading "name" Int (Reading "age" Int PureB)) Int
app = do
  s <- ask @"age"
  l <- ask @"name"
  pure (s + l)

result :: Int
result 
  = app 
  & runReader @"age" @"id" @Identity 18
  & runReader @"name" @"id" @Identity 20
  & runPure

The error:

*Main
<λ> result
<interactive>: internal error: stg_ap_p_ret
    (GHC version 8.2.1 for x86_64_unknown_linux)
    Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

Most of the code is the same as from this comment. A full paste can be found here.

Bug with variants -- almost certainly due to all these coercions :(

{-# LANGUAGE DataKinds,FlexibleContexts,KindSignatures,OverloadedLabels,TypeFamilies,TypeOperators #-}
{-# OPTIONS_GHC -fplugin=Coxswain -fconstraint-solver-iterations=1000 #-}

module Main where

import Data.Sculls.Symbol

vars :: [V I (Row0 .& "x" .= Int .& "z" .= Bool)]
vars = [inj #z True]

main :: IO ()
main = do
  print (head vars)
  print vars

prints

$ stack ghc -- -O --make Test.hs && ./Test.exe
[1 of 1] Compiling Main             ( Test.hs, Test.o )
...\Data\Sculls\Internal\RecordAndVariant.hi
Declaration for $w$cshow1
Unfolding of $w$cshow1:
  Iface id out of scope:  cobox
Linking Test.exe ...
<z True>
[<z False>]

I think the Iface id out of scope message is a red herring: it goes away if I remove the first print. (Edit: Wrong! I now think this is the key problem.)

This task is to explain this behavior and rectify it.

Make Core-lint happy

I've just been using stack on my laptop. So I currently haven't thrown coxswain to a debug-enabled ghc exe. I'm sure I don't have all the casts exactly right.

This task is to use such tooling in order to confirm that the plugin is correctly creating all the necessary coercions.

Either justify the roundabout `Ren` approach or replace it with something simpler

One consequence of this being a project I used to learn about the type checker and OutsideIn(X) is that there's plenty of design decisions I'm not sure about.

In particular, I don't have a rock solid motivation for using the Ren constraints instead of maintaining a separate and private substitution. I have a jumble of reasons why I think it might be better this way (not re-implementing unification, sharing knowledge with other plugins, avoiding loops where the plugin just keeps generating the same idempotent equality), but I really need to flesh them out and write up a good motivation for this approach.

`Includes` relation

I think that embedding one row in another can be done right now with type classes with the current basic interface, but I suspect that an Includes relation would be better behaved, especially alongside row polymorphism.

Includes p q would mean that p has every column that q has, enabling primitives like rupcast :: R f p -> R f q and vupcast :: V f q -> V f p. I anticipate that the necessary evidence would be a bitvector with as many bits as columns in p, each set if that field is in q.

Some non-trivial examples that I anticipate the plugin being able to decide:

Includes (p .& l .= t) p.
Includes (p .& l .= t1) (q .& l .= t2) implies t1 ~ t2.
Not Includes p (q .& l .= t) if Lacks p l.
Includes p q and Includes q r implies Includes p r.

(Is there a "closure" of this where a column in q can be present with a different type in p if it is a Row type and the column type in p Includes the column type in q?)

Support eliminating a variant with a record of functions with non-fixed codomain

I'm not sure if there's something fundamental preventing the inclusion of a function of type

vmap 
  :: Short (NumCols p - 1) 
  => R (f :->: g) p -> V f p -> V g p

in sculls.

One might then use a record of functions like

funcs :: R (I :->: I) (Row0 .& "int" .= Int .& "string" .= String)
funcs = mkR 
  .* (A (\(I x) -> I (2 * x)) :: (I :->: I) "int" Int)
  .* (A (\(I x) -> I (reverse x)) :: (I :->: I) "string" String)

to eliminate a variant like V I (Row0 .& "int" .= Int .& "string" .= String).

Unexpected errors when extending by the same field twice

Of course, mkR .* #x .= 'a' .* #x .= 'b' is wrong, but it would be nice if it gave a clear error and didn't defer it unexpectedly.

$ ghci -fplugin=Coxswain -XOverloadedLabels -XDataKinds -XTypeFamilies -XTypeOperators -XFlexibleContexts -fconstraint-solver-iterations=1000
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Prelude> :m + Data.Sculls.Symbol
Prelude Data.Sculls.Symbol> mkR .* #x .= 3 .* #x .= 4

<interactive>:1:1: error:
    Ambiguous type variables ‘t0’, ‘t1’ arising from a use of ‘print’
    prevents the constraint ‘(Data.Sculls.Internal.RecordAndVariant.RAll2
                                (ShowCol I)
                                (Normalize ((Row0 .& ("x" .= t0)) .& ("x" .= t1)))
                                2)’ from being solved.
    Probable fix: use a type annotation to specify what ‘t0’, ‘t1’ should be.
    These potential instance exist:
      instance forall kl kt (c :: kl
                                  -> kt -> Constraint) (l0 :: kl) (t0 :: kt) (l1 :: kl) (t1 :: kt).
               (c l0 t0, c l1 t1) =>
               Data.Sculls.Internal.RecordAndVariant.RAll2
                 c ('NExt ('NExt 'NRow0 l1 t1) l0 t0) 2
        -- Defined in ‘Data.Sculls.Internal.RecordAndVariant’
Prelude Data.Sculls.Symbol> mkR .* #x .= 'a' .* #x .= 'b' :: R I (Row0 .& "x" .= Char)
{(x=*** Exception: <interactive>:3:1: error:
    • No instance for (Lacks (Row0 .& ("x" .= Char)) "x")
        arising from a use of ‘.*’
    • In the expression:
          mkR .* #x .= 'a' .* #x .= 'b' :: R I (Row0 .& ("x" .= Char))
      In an equation for ‘it’:
          it = mkR .* #x .= 'a' .* #x .= 'b' :: R I (Row0 .& ("x" .= Char))
(deferred type error)

Pin down Derived constraints

I still don't feel confident about anticipating when, where, and why Derived constraints arise. For now, simplifyWanteds2 ignores them, and I'm pretty sure that's wrong.

A large part of the work for this task will be establishing a solid understanding of when/where/why Derived constraints arise. After we have that, I think adjusting the plugin won't be so much work.

Error messages mention unification (?) variables like `$coxswainTau0`

getAge :: (Lacks a "age", Short (NumCols a)) => R I (a .& "age" .= Int) -> Int
getAge = (`dot` #age)

getName :: (Lacks a "name", Short (NumCols a)) => R I (a .& "name" .= Text) -> Text
getName = (`dot` #name)

info :: _
info x = (getAge x, getName x)

The error:

src/Main.hs:47:9: error:
    • Found type wildcard ‘_’
        standing for ‘R I
                        (($coxswainTau0 .& ("name" .= Text)) .& ("age" .= Int))
                      -> (Int, Text)’
      Where: ‘$coxswainTau0’ is an ambiguous type variable
      To use the inferred type, enable PartialTypeSignatures
    • In the type signature: info :: _
   |
47 | info :: _
   |         ^
src/Main.hs:48:1: error:
    No instance for (Lacks $coxswainTau0 "age")
      arising from a use of ‘getAge’
   |
48 | info x = (getAge x, getName x)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Avoid panics on contradictions involving restriction skolems

Contradictions also need the deactivation pass of simplifyWanteds that replaces restriction skolems with restrictions of genuine skolems. This will prevent GHC from panicking when rendering the contradiction as an error message.

It'll take some doing though, so I'm deferring it for now.

Is `activateGivens` necessary/correct?

As with some other parts of the code -- which I was using to learn about the type checker --- this function seemed necessary/correct at one point, but subsequent refinements make me wonder if it's still necessary/correct.

Can we just drop it?
If not, should we be zonking them before activating them? Because what if they contain flattening skolems?

nfrisby / coxswain Goto Github PK

coxswain's People

Stargazers

Watchers

Forkers

coxswain's Issues

Recommend Projects

Recommend Topics

Recommend Org