search

Ferdinand-vW / sessiontypes

GNU General Public License v3.0
6 stars 2 forks source link

Build with GHC 9.2.5 #1

Closed asib closed 1 year ago

asib commented 1 year ago

Hello, very cool project! Appreciate that it's been untouched for a while so please ignore this if you're not interested in diving back into it.

I'm trying to build with LTS 20.11 (GHC 9.2.5) and facing a compilation error:

$ stack build
sessiontypes  > configure
sessiontypes  > Configuring sessiontypes-0.1.2...
sessiontypes  > build
sessiontypes  > Preprocessing library for sessiontypes-0.1.2..
sessiontypes  > Building library for sessiontypes-0.1.2..
sessiontypes  > [ 1 of 10] Compiling Control.SessionTypes.Indexed
sessiontypes  > [ 2 of 10] Compiling Control.SessionTypes.Types
sessiontypes  > 
sessiontypes  > /private/var/folders/5b/mf7yjff12qj98n08y3dcpm_h0000gn/T/stack-36fadf8e8a5d4101/sessiontypes-0.1.2/src/Control/SessionTypes/Types.hs:81:3: error:
sessiontypes  >     • Type family equation violates the family's injectivity annotation.
sessiontypes  >       Type variables ‘ctx’, ‘s’
sessiontypes  >       cannot be inferred from the right-hand side.
sessiontypes  >       Using UndecidableInstances might help
sessiontypes  >       In the type family equation:
sessiontypes  >         forall {c} {ctx :: [ST c]} {s :: ST c}.
sessiontypes  >           Dual ('Cap ctx s) = 'Cap (MapDual ctx) (DualST s)
sessiontypes  >             -- Defined at src/Control/SessionTypes/Types.hs:81:3
sessiontypes  >     • In the equations for closed type family ‘Dual’
sessiontypes  >       In the type family declaration for ‘Dual’
sessiontypes  >    |
sessiontypes  > 81 |   Dual ('Cap ctx s) = 'Cap (MapDual ctx) (DualST s)
sessiontypes  >    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
sessiontypes  > 
sessiontypes  > /private/var/folders/5b/mf7yjff12qj98n08y3dcpm_h0000gn/T/stack-36fadf8e8a5d4101/sessiontypes-0.1.2/src/Control/SessionTypes/Types.hs:85:3: error:
sessiontypes  >     • Type family equation violates the family's injectivity annotation.
sessiontypes  >       Type variable ‘r’ cannot be inferred from the right-hand side.
sessiontypes  >       Using UndecidableInstances might help
sessiontypes  >       In the type family equation:
sessiontypes  >         forall {c} {s :: c} {r :: ST c}.
sessiontypes  >           DualST (s ':!> r) = s ':?> DualST r
sessiontypes  >             -- Defined at src/Control/SessionTypes/Types.hs:85:3
sessiontypes  >     • In the equations for closed type family ‘DualST’
sessiontypes  >       In the type family declaration for ‘DualST’
sessiontypes  >    |
sessiontypes  > 85 |   DualST (s :!> r) = s :?> DualST r
sessiontypes  >    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
sessiontypes  > 
sessiontypes  > /private/var/folders/5b/mf7yjff12qj98n08y3dcpm_h0000gn/T/stack-36fadf8e8a5d4101/sessiontypes-0.1.2/src/Control/SessionTypes/Types.hs:86:3: error:
sessiontypes  >     • Type family equation violates the family's injectivity annotation.
sessiontypes  >       Type variable ‘r’ cannot be inferred from the right-hand side.
sessiontypes  >       Using UndecidableInstances might help
sessiontypes  >       In the type family equation:
sessiontypes  >         forall {c} {s :: c} {r :: ST c}.
sessiontypes  >           DualST (s ':?> r) = s ':!> DualST r
sessiontypes  >             -- Defined at src/Control/SessionTypes/Types.hs:86:3
sessiontypes  >     • In the equations for closed type family ‘DualST’
sessiontypes  >       In the type family declaration for ‘DualST’
sessiontypes  >    |
sessiontypes  > 86 |   DualST (s :?> r) = s :!> DualST r
sessiontypes  >    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
sessiontypes  > 
sessiontypes  > /private/var/folders/5b/mf7yjff12qj98n08y3dcpm_h0000gn/T/stack-36fadf8e8a5d4101/sessiontypes-0.1.2/src/Control/SessionTypes/Types.hs:87:3: error:
sessiontypes  >     • Type family equation violates the family's injectivity annotation.
sessiontypes  >       Type variable ‘xs’ cannot be inferred from the right-hand side.
sessiontypes  >       Using UndecidableInstances might help
sessiontypes  >       In the type family equation:
sessiontypes  >         forall {a} {xs :: [ST a]}.
sessiontypes  >           DualST ('Sel xs) = 'Off (MapDual xs)
sessiontypes  >             -- Defined at src/Control/SessionTypes/Types.hs:87:3
sessiontypes  >     • In the equations for closed type family ‘DualST’
sessiontypes  >       In the type family declaration for ‘DualST’
sessiontypes  >    |
sessiontypes  > 87 |   DualST (Sel xs)  = Off (MapDual xs)
sessiontypes  >    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
sessiontypes  > 
sessiontypes  > /private/var/folders/5b/mf7yjff12qj98n08y3dcpm_h0000gn/T/stack-36fadf8e8a5d4101/sessiontypes-0.1.2/src/Control/SessionTypes/Types.hs:88:3: error:
sessiontypes  >     • Type family equation violates the family's injectivity annotation.
sessiontypes  >       Type variable ‘xs’ cannot be inferred from the right-hand side.
sessiontypes  >       Using UndecidableInstances might help
sessiontypes  >       In the type family equation:
sessiontypes  >         forall {a} {xs :: [ST a]}.
sessiontypes  >           DualST ('Off xs) = 'Sel (MapDual xs)
sessiontypes  >             -- Defined at src/Control/SessionTypes/Types.hs:88:3
sessiontypes  >     • In the equations for closed type family ‘DualST’
sessiontypes  >       In the type family declaration for ‘DualST’
sessiontypes  >    |
sessiontypes  > 88 |   DualST (Off xs)  = Sel (MapDual xs)
sessiontypes  >    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
sessiontypes  > 
sessiontypes  > /private/var/folders/5b/mf7yjff12qj98n08y3dcpm_h0000gn/T/stack-36fadf8e8a5d4101/sessiontypes-0.1.2/src/Control/SessionTypes/Types.hs:89:3: error:
sessiontypes  >     • Type family equation violates the family's injectivity annotation.
sessiontypes  >       Type variable ‘s’ cannot be inferred from the right-hand side.
sessiontypes  >       Using UndecidableInstances might help
sessiontypes  >       In the type family equation:
sessiontypes  >         forall {a} {s :: ST a}.
sessiontypes  >           DualST ('R s) = 'R (DualST s)
sessiontypes  >             -- Defined at src/Control/SessionTypes/Types.hs:89:3
sessiontypes  >     • In the equations for closed type family ‘DualST’
sessiontypes  >       In the type family declaration for ‘DualST’
sessiontypes  >    |
sessiontypes  > 89 |   DualST (R s)     = R (DualST s)
sessiontypes  >    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
sessiontypes  > 
sessiontypes  > /private/var/folders/5b/mf7yjff12qj98n08y3dcpm_h0000gn/T/stack-36fadf8e8a5d4101/sessiontypes-0.1.2/src/Control/SessionTypes/Types.hs:90:3: error:
sessiontypes  >     • Type family equation violates the family's injectivity annotation.
sessiontypes  >       Type variable ‘s’ cannot be inferred from the right-hand side.
sessiontypes  >       Using UndecidableInstances might help
sessiontypes  >       In the type family equation:
sessiontypes  >         forall {a} {s :: ST a}.
sessiontypes  >           DualST ('Wk s) = 'Wk (DualST s)
sessiontypes  >             -- Defined at src/Control/SessionTypes/Types.hs:90:3
sessiontypes  >     • In the equations for closed type family ‘DualST’
sessiontypes  >       In the type family declaration for ‘DualST’
sessiontypes  >    |
sessiontypes  > 90 |   DualST (Wk s)    = Wk (DualST s)
sessiontypes  >    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
sessiontypes  > 
sessiontypes  > /private/var/folders/5b/mf7yjff12qj98n08y3dcpm_h0000gn/T/stack-36fadf8e8a5d4101/sessiontypes-0.1.2/src/Control/SessionTypes/Types.hs:97:3: error:
sessiontypes  >     • Type family equation violates the family's injectivity annotation.
sessiontypes  >       Type variables ‘s’, ‘xs’
sessiontypes  >       cannot be inferred from the right-hand side.
sessiontypes  >       Using UndecidableInstances might help
sessiontypes  >       In the type family equation:
sessiontypes  >         forall {c} {s :: ST c} {xs :: [ST c]}.
sessiontypes  >           MapDual (s : xs) = DualST s : MapDual xs
sessiontypes  >             -- Defined at src/Control/SessionTypes/Types.hs:97:3
sessiontypes  >     • In the equations for closed type family ‘MapDual’
sessiontypes  >       In the type family declaration for ‘MapDual’
sessiontypes  >    |
sessiontypes  > 97 |   MapDual (s ': xs) = DualST s ': MapDual xs
sessiontypes  >    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Progress 1/2

Error: [S-7282]
       Stack failed to execute the build plan.

       While executing the build plan, Stack encountered the following errors:

       [S-7011]
       While building package sessiontypes-0.1.2 (scroll up to its section to see the error) using:
       /Users/jacobfenton/.stack/setup-exe-cache/aarch64-osx/Cabal-simple_SvXsv1f__3.6.3.0_ghc-9.2.5 --verbose=1 --builddir=.stack-work/dist/aarch64-osx/Cabal-3.6.3.0 build --ghc-options " -fdiagnostics-color=always"
       Process exited with code: ExitFailure 1

If I add UndecidableInstances as GHC suggests and rebuild I get the following compilation error:

$ stack build
Building all executables for `sessiontypes' once. After a successful build of all of them, only specified executables will be rebuilt.
sessiontypes> build (lib + exe)
Preprocessing library for sessiontypes-0.1.2..
Building library for sessiontypes-0.1.2..
[ 4 of 10] Compiling Control.SessionTypes.STTerm

/Users/jacobfenton/Desktop/sessiontypes/src/Control/SessionTypes/STTerm.hs:57:12: error:
    • Expected a type, but ‘a’ has kind ‘a’
    • In the type ‘(a -> STTerm m ('Cap ctx r) r' b)’
      In the definition of data constructor ‘Recv’
      In the data declaration for ‘STTerm’
   |
57 |   Recv :: (a -> STTerm m ('Cap ctx r) r' b) -> STTerm m ('Cap ctx (a :?> r)) r' b
   |            ^

Error: [S-7282]
       Stack failed to execute the build plan.

       While executing the build plan, Stack encountered the following errors:

       [S-7011]
       While building package sessiontypes-0.1.2 (scroll up to its section to see the error) using:
       /Users/jacobfenton/.stack/setup-exe-cache/aarch64-osx/Cabal-simple_SvXsv1f__3.6.3.0_ghc-9.2.5 --verbose=1 --builddir=.stack-work/dist/aarch64-osx/Cabal-3.6.3.0 build lib:sessiontypes exe:test-visualizer --ghc-options " -fdiagnostics-color=always"
       Process exited with code: ExitFailure 1

I'll confess I'm not a Haskell expert but I can't understand why GHC thinks the kind of a is a and not *.

I should add I'm using 9.2.5 because I'm on an M1 mac and trying to avoid rebuilding the version of GHC used by this library.

Ferdinand-vW commented 1 year ago

Hey!

Thanks for checking it out. I managed to resolve the issue but following the errors. Besides UndecidableInstances pragma it also required RankNTypes with a forall scope in the definition of STTerm. I managed to get there by following the errors, but it's not quite clear to me why the forall is necessary now and not before.

The fix is merged to master so feel free to check it out again.

Ferdinand-vW commented 1 year ago

Ah it seems to be due to these changes:

https://downloads.haskell.org/ghc/8.10.1/docs/html/users_guide/8.10.1-notes.html

GHC now performs more validity checks on inferred type signatures. One consequence of this change is that some programs that used to be accepted will no longer compile without enabling the required language extensions. For example, in these two modules:

{-# LANGUAGE RankNTypes #-}
module A where

  foo :: (forall a. a -> a) -> b -> b
  foo f x = f x

module B where

  import A

  bar = foo

Notice that A enables -XRankNTypes, but B does not. Previous versions of GHC would allow bar to typecheck, even though its inferred type is higher-rank. GHC 8.10 will now reject this, as one must now enable -XRankNTypes in B to accept the inferred type signature.

Type family dependencies (also known as injective type families) sometimes now need -XUndecidableInstances in order to be accepted. Here is an example:

type family F1 a = r | r -> a
type family F2 a = r | r -> a
type instance F2 [a] = Maybe (F1 a)

Because GHC needs to look under a type family to see that a is determined by the right-hand side of F2‘s equation, this now needs -XUndecidableInstances. The problem is very much akin to its need to detect some functional dependencies.

asib commented 1 year ago

Awesome, thanks so much for pushing the fix and explaining it!