silence the plugin

Author: ekmett

src/Linear/Logic/Functor.hs

@@ -30,7 +30,7 @@
 {-# language UndecidableSuperClasses #-}
 {-# language ImportQualifiedPost #-}
 {-# language Trustworthy #-}
-{-# options_ghc -fplugin Linear.Logic.Plugin #-} -- TODO use this to kill Prep constraints
+-- {-# options_ghc -fplugin Linear.Logic.Plugin #-} -- TODO use this to kill Prep constraints
 
 -- {-# options_ghc -Wno-unused-imports #-}
 
@@ -142,8 +142,10 @@ instance Category (FUN 'One) where
 -- | Here we have the ability to provide more refutations, because we can walk
 -- all the way back to my arrows. This is internal to my logic.
 class (forall a b. (Prop' a, Prop' b) => Prop' (p a b)) => NiceCategory p where
+  -- o :: p b c ⊸ p a b ⊸ p a c 
   o :: (Lol l, Lol l', Prop a, Prop b, Prop c) => l (p b c) (l' (p a b) (p a c))
 
+
 instance Category (⊸) where
   id = Lol \case L -> \x -> x; R -> \x -> x
   f . g = Lol \case

src/Linear/Logic/Internal.hs

@@ -63,7 +63,7 @@ class Prep a => Prop' a where
   -- @
   (!=) :: a %1 -> Not a %1 -> r
 
--- avoids UndecidableSuperClasses:w
+-- avoids UndecidableSuperClasses
 type Prop a = (Prop' a, Prop' (Not a))
 
 -- | The unit for multiplicative conjunction, \(\texttt{()}\)
@@ -379,6 +379,14 @@ instance Prep a => Prop' (WhyNot a) where
   f != Ur a = because f a
   {-# inline (!=) #-}
 
+-- |
+-- @
+-- data DSum f g where
+--   (:=>) :: !(f a) -> g a -> DSum f g
+
+-- DSum (Y a b) Identity ~ Either a b
+-- DWith (Y a b) Identity ~ a & b
+-- @
 newtype DWith f g = DWith (forall x. f x %1 -> g x)
 
 dwith :: (forall x. f x %1 -> g x) %1 -> DWith f g

src/Linear/Logic/Plugin.hs

@@ -102,14 +102,14 @@ solveLogic () givens _deriveds wanteds = do
         , Just (n2, [x]) <- splitTyConApp_maybe nx, hasKey n2 notKey
         -> do
           wantedEvidence <- newWanted (ctLoc ct) $ mkTyConApp eqPrimTyCon [liftedTypeKind,liftedTypeKind,x,y]
-          io $ putStrLn $ "not-not: " ++ pp nnx ++ " ~ " ++ pp y ++ " if " ++ pp x ++ " ~ " ++ pp y
+          -- io $ putStrLn $ "not-not: " ++ pp nnx ++ " ~ " ++ pp y ++ " if " ++ pp x ++ " ~ " ++ pp y
           pure ([(evByFiat "not-not" nnx y, ct)],[mkNonCanonical wantedEvidence])
       EqPred NomEq y nnx
         | Just (n1, [nx]) <- splitTyConApp_maybe nnx, hasKey n1 notKey
         , Just (n2, [x]) <- splitTyConApp_maybe nx, hasKey n2 notKey
         -> do
           wantedEvidence <- newWanted (ctLoc ct) $ mkTyConApp eqPrimTyCon [liftedTypeKind,liftedTypeKind,x,y]
-          io $ putStrLn $ "not-not: " ++ pp y ++ " ~ " ++ pp nnx ++ " if " ++ pp x ++ " ~ " ++ pp y
+          -- io $ putStrLn $ "not-not: " ++ pp y ++ " ~ " ++ pp nnx ++ " if " ++ pp x ++ " ~ " ++ pp y
           pure ([(evByFiat "not-not" nnx y, ct)],[mkNonCanonical wantedEvidence])
       EqPred NomEq nx y 
         | Just (n1, [x]) <- splitTyConApp_maybe nx, hasKey n1 notKey
@@ -131,7 +131,7 @@ solveLogic () givens _deriveds wanteds = do
             (ctLoc ct) 
             (mkTyConApp eqPrimTyCon [liftedTypeKind,liftedTypeKind,nnx,x]) 
             (runEvExpr $ evByFiat "not-not-ish" nnx x)
-          io $ putStrLn $ "not-notish: " ++ pp nnx ++ " ~# " ++ pp x
+          -- io $ putStrLn $ "not-notish: " ++ pp nnx ++ " ~# " ++ pp x
           pure ([],[mkNonCanonical givenEvidence])
       EqPred n x y -> do
        -- io $ putStrLn $ "I think " ++ pp n ++ " " ++ pp x ++ pp y ++ " is none of my business"
@@ -141,7 +141,7 @@ solveLogic () givens _deriveds wanteds = do
         , Just (n1, [nx]) <- splitTyConApp_maybe nnx, hasKey n1 notKey
         , Just (n2, [x]) <- splitTyConApp_maybe nx, hasKey n2 notKey
         -> do
-        io $ putStrLn $ "Ooh ooh ooh: " ++ show (pp c, pp x, pp y)
+        -- io $ putStrLn $ "Ooh ooh ooh: " ++ show (pp c, pp x, pp y)
         wantedEvidence <- newWanted (ctLoc ct) $ mkTyConApp eqPrimTyCon [liftedTypeKind,liftedTypeKind,x,y]