Type-signature from `:type` doesn't type-check


#1

Brian Marick [5:35 PM]

Type annotation fails for `_element = at`; succeeds for `_element x = at x` 
I import `at` from purescript-profunctor-lens
  import Data.Lens.At (at)
I define a synonym:
  _element = at
I find its type:
  > :t _element
  forall b a m. At m a b => a -> (forall p. Strong p => p (Maybe b) (Maybe b) -> p m m)
I add it as a type annotation:
  _element :: forall b a m. At m a b => a -> (forall p. Strong p => p (Maybe b) (Maybe b) -> p m m)
  _element = at
But the compiler rejects it:
 Could not match constrained type
                           
  Strong t3 => t3 (Maybe t4) (Maybe t4) -> t3 t5 t5
                           
 with type
                           
  Strong p6 => p6 (Maybe b1) (Maybe b1) -> p6 m2 m2
                           
while trying to match type Strong t3 => t3 (Maybe t4) (Maybe t4) -> t3 t5 t5
 with type Strong p6 => p6 (Maybe b1) (Maybe b1) -> p6 m2 m2
while checking that expression at
 has type a0 -> (forall p. Strong p => p (Maybe b1) (Maybe b1) -> p m2 m2)
in value declaration _element
where m2 is a rigid type variable
    bound at line 75, column 12 - line 75, column 12
   a0 is a rigid type variable
    bound at line 75, column 12 - line 75, column 12
   b1 is a rigid type variable
    bound at line 75, column 12 - line 75, column 12
   p6 is a rigid type variable
   t5 is an unknown type
   t4 is an unknown type
   t3 is an unknown type
Note that the problem goes away if you add an explicit argument:
_element :: forall b a m. At m a b => a -> (forall p. Strong p => p (Maybe b) (Maybe b) -> p m m) 
_element x = at x

In this case, why is what :type produces not accepted as a type
annotation? (using both 0.11.7 and 0.12)

chexxor [5:37 PM]
Can a higher-ranked argument have constraints?
I’ve never tried it before
Ah yeah, it’s just a type synonym there
that’s neat

garyb [5:45 PM]
@Brian Marick you can probably work around this by “eta expanding” the definition, like _element a = at a… I’m not sure why, but it’s a problem I’ve run into in the past too, I opened an issue about it, but I don’t remember it making the situation any clearer for me :wink:

garyb [5:45 PM]
@Brian Marick here’s the issue with some description, but it’s mainly about the typechecker internals https://github.com/purescript/purescript/issues/950 (edited)