search

UlfNorell / insane

Toy typechecker for Insanely Dependent Types
79 stars 4 forks source link

Code does not build with GHC 8.6.5, does not list which version of GHC is needed #2

Open JasonGross opened 1 year ago

JasonGross commented 1 year ago 
$ make
ghc --make -o tc Main.hs -fwarn-incomplete-patterns -Werror

TypeChecker.hs:1:55: error: [-Werror]
    -XOverlappingInstances is deprecated: instead use per-instance pragmas OVERLAPPING/OVERLAPPABLE/OVERLAPS
  |
1 | {-# LANGUAGE UndecidableInstances, FlexibleInstances, OverlappingInstances #-}
  |                                                       ^^^^^^^^^^^^^^^^^^^^
make: *** [Makefile:25: tc] Error 1

If I disable that, I get

$ make ghc_flags=-fwarn-incomplete-patterns
make -C typechecker
make[1]: Entering directory '/home/jgross/Documents/GitHub/insane/typechecker'
ghc --make -o tc Main.hs -fwarn-incomplete-patterns

TypeChecker.hs:1:55: warning:
    -XOverlappingInstances is deprecated: instead use per-instance pragmas OVERLAPPING/OVERLAPPABLE/OVERLAPS
  |
1 | {-# LANGUAGE UndecidableInstances, FlexibleInstances, OverlappingInstances #-}
  |                                                       ^^^^^^^^^^^^^^^^^^^^

TypeChecker/Force.hs:1:55: warning:
    -XOverlappingInstances is deprecated: instead use per-instance pragmas OVERLAPPING/OVERLAPPABLE/OVERLAPS
  |
1 | {-# LANGUAGE FlexibleInstances, UndecidableInstances, OverlappingInstances #-}
  |                                                       ^^^^^^^^^^^^^^^^^^^^

TypeChecker/Print.hs:1:55: warning:
    -XOverlappingInstances is deprecated: instead use per-instance pragmas OVERLAPPING/OVERLAPPABLE/OVERLAPS
  |
1 | {-# LANGUAGE FlexibleInstances, UndecidableInstances, OverlappingInstances #-}
  |                                                       ^^^^^^^^^^^^^^^^^^^^

TypeChecker/DeBruijn.hs:1:55: warning:
    -XOverlappingInstances is deprecated: instead use per-instance pragmas OVERLAPPING/OVERLAPPABLE/OVERLAPS
  |
1 | {-# LANGUAGE FlexibleInstances, UndecidableInstances, OverlappingInstances #-}
  |                                                       ^^^^^^^^^^^^^^^^^^^^
[11 of 19] Compiling TypeChecker.Monad.Heap ( TypeChecker/Monad/Heap.hs, TypeChecker/Monad/Heap.o )

TypeChecker/Monad/Heap.hs:84:5: error:
    • Could not deduce (Control.Monad.Fail.MonadFail TC)
        arising from a do statement
        with the failable pattern ‘Evaluated x’
      from the context: Pointer ptr a
        bound by the type signature for:
                   forceClosure :: forall ptr a. Pointer ptr a => ptr -> TC a
        at TypeChecker/Monad/Heap.hs:82:1-44
    • In a stmt of a 'do' block: Evaluated x <- modClosure eval p
      In the expression:
        do Evaluated x <- modClosure eval p
           return x
      In an equation for ‘forceClosure’:
          forceClosure p
            = do Evaluated x <- modClosure eval p
                 return x
            where
                eval cl@(Evaluated _) = return cl
                eval (Unevaluated m)
                  = do x <- runTCClosure m
                       ....
   |
84 |     Evaluated x <- modClosure eval p
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
make[1]: *** [Makefile:25: tc] Error 1
make[1]: Leaving directory '/home/jgross/Documents/GitHub/insane/typechecker'
make: *** [Makefile:3: default] Error 2

What version of ghc should I be using? Or would it be possible to update the project for newer ghc?

JasonGross commented 1 year ago

Here is a patch that makes things compile, with warnings:

diff --git a/typechecker/TypeChecker.hs b/typechecker/TypeChecker.hs
index 3927ce5..aa2fc26 100644
--- a/typechecker/TypeChecker.hs
+++ b/typechecker/TypeChecker.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE UndecidableInstances, FlexibleInstances, OverlappingInstances #-}
+{-# LANGUAGE UndecidableInstances, FlexibleInstances, OverlappingInstances, FlexibleContexts #-}

 module TypeChecker where

@@ -238,7 +238,7 @@ checkPattern p a ret =
         apps s (t:ts) = do
             st <- evaluated (App s t)
             apps st ts
-        
+

 isType :: Abs.Expr -> TC Type
 isType e = suspend (isType' e)
@@ -430,4 +430,3 @@ instance (Convert a, Convert b) => Convert (a,b) where

 instance Convert a => Convert (Abs a) where
     (===) = (===) `on` absBody
-
diff --git a/typechecker/TypeChecker/Monad.hs b/typechecker/TypeChecker/Monad.hs
index 556723b..b32275d 100644
--- a/typechecker/TypeChecker/Monad.hs
+++ b/typechecker/TypeChecker/Monad.hs
@@ -7,6 +7,7 @@ import Control.Applicative
 import Control.Monad.State
 import Control.Monad.Reader
 import Control.Monad.Error
+import Control.Monad.Fail
 import Data.Map as Map
 import Data.Dynamic

@@ -130,7 +131,7 @@ instance Error TCError where
 ---------------------------------------------------------------------------

 newtype TC a = TC { unTC :: ReaderT TCEnv (ErrorT TCError (StateT TCState IO)) a }
-    deriving (Functor, MonadReader TCEnv, MonadState TCState, MonadError TCError, MonadIO, Monad)
+    deriving (Functor, MonadReader TCEnv, MonadState TCState, MonadError TCError, MonadIO, Monad, MonadFail)

 instance Applicative TC where
   pure  = return
@@ -142,4 +143,3 @@ runTC (TC m) =
     runErrorT            $
     flip runReaderT emptyEnv  $
     m
-
diff --git a/typechecker/TypeChecker/Print.hs b/typechecker/TypeChecker/Print.hs
index 03984ab..35a36dd 100644
--- a/typechecker/TypeChecker/Print.hs
+++ b/typechecker/TypeChecker/Print.hs
@@ -59,7 +59,7 @@ instance Pretty Definition where
         ]

 instance Pretty Constructor where
-    pretty (Constr c ar) = text c <> text "/" <> text (show ar)
+    pretty (Constr c ar) = text c TypeChecker.Print.<> text "/" TypeChecker.Print.<> text (show ar)

 instance Pretty Clause' where
     pretty (Clause ps t) =
@@ -106,7 +106,7 @@ instance Pretty Term' where
        sep [ prettyPrec 5 s, prettyPrec 6 t ]
    Lam t   ->
        mparens (n > 0) $
-       sep [ text "\\" <> text (absName t) <+> text "->"
+       sep [ text "\\" TypeChecker.Print.<> text (absName t) <+> text "->"
        , nest 2 $ pretty t
        ]

@@ -122,4 +122,3 @@ prettyPat n p ret = case p of

 instance Pretty a => Pretty (Abs a) where
     prettyPrec n (Abs x b) = extendContext_ x $ prettyPrec n b
-
diff --git a/typechecker/TypeChecker/Reduce.hs b/typechecker/TypeChecker/Reduce.hs
index b0bced2..db687d3 100644
--- a/typechecker/TypeChecker/Reduce.hs
+++ b/typechecker/TypeChecker/Reduce.hs
@@ -73,6 +73,11 @@ conView t = do

 data Progress = NoProgress | YesProgress

+instance Semigroup Progress where
+    NoProgress <> p        = p
+    p <> NoProgress        = p
+    YesProgress <> YesProgress = YesProgress
+
 instance Monoid Progress where
     mempty             = NoProgress
     mappend NoProgress p       = p
@@ -126,6 +131,13 @@ instance WHNF Term where

 data Match a = YesMatch a | MaybeMatch | NoMatch

+instance Semigroup a => Semigroup (Match a) where
+    NoMatch <> _    = NoMatch
+    _ <> NoMatch    = NoMatch
+    MaybeMatch <> _ = MaybeMatch
+    _ <> MaybeMatch = MaybeMatch
+    (YesMatch ts) <> (YesMatch ss) = YesMatch $ ts Data.Monoid.<> ss
+
 instance Monoid a => Monoid (Match a) where
     mempty      = YesMatch mempty
     mappend NoMatch _   = NoMatch
@@ -178,4 +190,3 @@ matchPattern (ConP c ps) t = do
    _       -> return MaybeMatch
   where
     dropPars ts = drop (length ts - length ps) ts
-