bsc Internal Compiler error

[bpfoley]

The following

package ZipCrash where

import List

class Functor f where
  map :: (a -> b) -> f a -> f b

class Zip f where
  toListX   :: f a -> List a
  fromListX :: List a -> f a

  zipXWith :: (a -> b -> c) -> f a -> f b -> f c
  zipXWith f xs ys = fromListX (List.zipWith f (toListX xs) (toListX ys))

interface Bar at bt =
  a :: at
  b :: bt

type Foo t = Bar t t

instance Functor Foo where
  map f x = Foo (f x.a) (f x.b)

instance Zip Foo where
  zipXWith f x y = Foo (f x.a y.a) (f x.b y.b)

causes bsc ZipCrash.bs to crash with

Internal Bluespec Compiler Error:
Please report this failure to your Bluespec technical contact.
If you do not know your contact, you may email support@bluespec.com.
The following internal error message should be included in your
correspondence along with any other relevant details:
Bluespec Compiler (build 02ff76b)
expandSyn,truncType
(1, 0, ZipCrash.Functor ZipCrash.Foo, ZipCrash.Bar (TGen 0) (TGen 0))

[bpfoley]

NB this also crashes with bsc v2018_08_gx3

[quark17]

As @nanavati says in the duplicate #242 , this source isn't legal because it contains a partially-applied type synonym, and BSC should report that as a user error (not an internal error).

The example has this type:

interface Bar at bt =
  a :: at
  b :: bt

And it'd like to declare an instance for the typeclass Functor (which expects a constructor of only one argument) when the types of the two arguments are the same. If BSC had a way to declare a type-lambda, we might be able to say this:

instance Functor (\t -> Bar t t) where ...

But this isn't supported. So the example tries to use a type synonym:

type Foo t = Bar t t
instance Functor Foo where ...

However, this also doesn't work because type synonyms have no substance, they are merely syntactic sugar. They don't represent type functions (although maybe that's an improvement to consider?).

The error EPartialTypeApp exists for reporting partially applied type synonyms. It's used elsewhere in MakeSymTab, but it seems like convInst should be checking for this (or using a function that checks for it) too.

[bpfoley]

So... let me see if I understand this correctly. In a sense type synonyms are just "macros" that are expanded in place?

So

instance Functor Foo where
    map f x = Foo (f x.a) (f x.b)

actually expands out to

instance Functor Bar where
    map f x = Bar (f x.a) (f x.b)

But the typeclass Functor only has one type parameter, and Bar has two, so Bar's second parameter isn't bound?

[quark17]

Yes, they are just macros, and it should be safe for BSC to substitute them away entirely before doing actual typecheck.

However, the example does not expand as you've described. BSC only ever expands Foo <arg> to Bar <arg> <arg>. If BSC were behaving properly, it would report a user error in this case, that Foo cannot be partially applied. (BSC will not expand the partial application to anything.)

While it should be safe for BSC to expand away all type synonyms as a first pass, I believe that BSC does not do this. I believe that BSC makes some attempt to keep the synonyms around until the last minute, so that other error messages can be better reported in terms of the original names.

So there are places in BSC's source code that apply type synonyms when necessary. I would guess that the internal error occurs because the substitution code does not expect to encounter a partially-applied synonym; the code expects that an earlier step has checked for this case and warned about it. I believe that BSC does check for this in ordinary definitions, but has perhaps not been properly looking for it in instance definitions. The fix for this bug may simply be to improve the current check to also apply to the types of typeclass instance definitions.

(FYI, there are some places where BSC ought to be expanding away type synonyms but currently is not, because we discovered that some library code had been relying on erroneous matching of the synonym structure! We discovered this when we attempted to fix BSC to properly expand the synonyms, but we backed it out until we could figure out how to not affect users of the library. I don't think that was ever resolved. See the XXX comments in TCheck and CtxRed that say "disable expanding of type synonyms until failures with TLM instances are resolved". I believe that if you reinstate that code, you'll see failures when compiling one or both of the TLM libraries.)

[blackgnezdo]

I just hit this again, so here's a shorter reproducer I found:

package Test where

import Assert
type Identity a = a
struct W a = { unW :: a Bool } deriving (Bits)
type X = W Identity

assertSize :: (IsModule m c) => m Empty
assertSize = do
  let x = valueOf (SizeOf (X))
  staticAssert (x == 1) "SizeOf X"

This fails with:

Bluespec Compiler, version untagged-g6770d36 (build 6770d36)
expandSyn,truncType
(1, 0, Prelude.SizeOf SimR2Test.X, (TGen 0))