Additional Unit argument makes a module compile

Help
#1

Hi,

TLDR: adding a unit parameter to a function makes the previously-rejected code compile.

Sorry for no minimal example, but as we do some complicated typelevel things in our project, producing such an example would be difficult. Let’s try.

I have a data type

newtype CellRenderer :: Type -> Type -> Symbol -> Type -> Row Type -> Type
newtype CellRenderer w i lab a r = CellRenderer ...

where lab is a shadow type (some record label). I have defined two smart constructors:

mkNoCellRenderer :: forall w i lab a r. CellRenderer w i lab a r
mkNoCellRenderer = CellRenderer ...

mkNoCellRenderer' :: forall w i lab a r. Unit -> CellRenderer w i lab a r
mkNoCellRenderer' _ = <same code as above>

In some contexts, using the first function gives errors like Could not match type lab7 with type "entity". However, using the second function (the same code but with additional ignored unit parameter) makes it compile.

Are you aware in which contexts those two functions can be different? Again, sorry for not giving more specific example, but extracting something easy to follow would take some time.

1 Like
#2

I noticed what fixes it. The erroring code looks like this:

test = someFunc { entity: mkNoCellRenderer }

however, when I change it to declaration - and - application,

test' = someFunc test
test = { entity: mkNoCellRenderer }

it compiles. I guess it has something to do with forall quantifiers floating from the field declaration to the whole record declaration, but I’m not sure.

1 Like
#3

Ok, I have a minimal example:

data X lab a = X (a -> String)

mkX :: forall lab a. X lab a
mkX = X (const "Example")

test = { example: mkX }

func :: forall a lab r rt. Cons lab (X lab a) rt r => IsSymbol lab => Proxy lab -> Record r -> a -> String
func lab r v = f v
  where X f = get lab r

-- example = func (Proxy :: Proxy "example") { example: mkX }
example = func (Proxy :: Proxy "example") test

The second example compiles, the first doesn’t. However, when I change mkX adding Unit argument,

mkX :: forall lab a. Unit -> X lab a
mkX _ = X (const "Example")

test = { example: mkX unit }

example' = func (Proxy :: Proxy "example") { example: mkX unit }
example = func (Proxy :: Proxy "example") test

both examples compile.

1 Like
#4

Here are a few ways to resolve it.

example = func (Proxy :: Proxy "example") ({ example: mkX } :: forall lab a. { example :: X lab a })

example = func (Proxy :: Proxy "example") { example: mkX :: _ }

example = func (Proxy :: Proxy "example") (identity { example: mkX })

example = func (Proxy :: Proxy "example") { example: identity mkX }

I believe this is the result of this inference rule, which I’ve wanted to remove for a long time.

Basically, the compiler is inferring too much polymorphism in record constructors. In this case it’s moving the forall under the record field because mkX is a bare var ({ example :: forall .... }). Any of the above solutions work around the inference rule (it either has a signature, or it’s no longer a bare var).

The main issue with removing this rule, is that it would be considered a breaking change, and there are some corner cases that will fail to typecheck.

1 Like
#5

Thanks! Yes, after reading through the error messages, I had the feeling that something like that happens. Is it really desirable? I mean do the language maintainers prefer to have it like that and not to break some other corner cases you mention? What are those?

Edit: why does it work when I split the definition of example into definition of test and applied func, although I don’t specify any type signatures?

#6

If you look at the inferred type of test it’s equivalent to forall lab a. { example :: X lab a } which matches my first example above. This is another reason why I want to remove that inference rule, since it’s different than top-level generalization.

I think it just exists to prevent some old code from breaking (I think around the 0.8 release? I don’t remember exactly). I personally don’t think it’s desirable and the result is more confusing than beneficial. I think if we removed it, we should look at how to push down more type information, because you should assume that anything requiring polymorphic record field members will need a more direct annotation. This may require something similar to GHC’s QuickLook impredicativity.

1 Like