Opened 5 months ago

Last modified 5 months ago

#13778 new bug

explicitly bidirectional patterns should not report Recursive definition" when used in view pattern expression position

Reported by: heisenbug Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.3
Keywords: PatternSynonyms Cc: Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Compile this

pattern One <- ((==One) -> True)
  where One = 1

I get

test.hs:1:1: error:  
    Recursive pattern synonym definition with following bindings:
      One (defined at test.hs:(1,1)-(1,15))
  |
Compilation failed.

Note that the error is due to the usage in view pattern expression position.

But for explicitly bidirectional patterns, there is no recursivity going on. So this usage should be allowed.

I am testing with HEAD, but the issue is probably older.

Change History (4)

comment:1 Changed 5 months ago by Iceland_jack

Cc: Iceland_jack added

This would be good to have

comment:2 Changed 5 months ago by simonpj

Harump. I think you want

  1. To infer the type of One from its "builder"
      One = 1
    
  1. To use that type when inferring the type of the pattern

But actually GHC does it the other way round

  1. Infer the type of the pattern
  2. Use that in checking the type of the "builder"

There's a good reason for this. Here's a Note from RnBinds:

Note [Pattern synonym builders don't yield dependencies]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When renaming a pattern synonym that has an explicit builder,
references in the builder definition should not be used when
calculating dependencies. For example, consider the following pattern
synonym definition:

pattern P x <- C1 x where
  P x = f (C1 x)

f (P x) = C2 x

In this case, 'P' needs to be typechecked in two passes:

1. Typecheck the pattern definition of 'P', which fully determines the
   type of 'P'. This step doesn't require knowing anything about 'f',
   since the builder definition is not looked at.

2. Typecheck the builder definition, which needs the typechecked
   definition of 'f' to be in scope; done by calls oo tcPatSynBuilderBind
   in TcBinds.tcValBinds.

This behaviour is implemented in 'tcValBinds', but it crucially
depends on 'P' not being put in a recursive group with 'f' (which
would make it look like a recursive pattern synonym a la 'pattern P =
P' which is unsound and rejected).

So I don't see an easy way to give you want you want.

The only think I can think of is to allow some kind of monomorphic recursion. But it's easy to program around, so I'm disinclined to fiddle.

comment:3 in reply to:  2 Changed 5 months ago by heisenbug

Replying to simonpj:

Hi Simon, adding a type signature won't make the error go away. IIRC this is not a type inference problem. I cannot try now, am AFK.

Harump. I think you want

  1. To infer the type of One from its "builder"
      One = 1
    
  1. To use that type when inferring the type of the pattern

But actually GHC does it the other way round

  1. Infer the type of the pattern
  2. Use that in checking the type of the "builder"

There's a good reason for this. Here's a Note from RnBinds:

Note [Pattern synonym builders don't yield dependencies]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When renaming a pattern synonym that has an explicit builder,
references in the builder definition should not be used when
calculating dependencies. For example, consider the following pattern
synonym definition:

pattern P x <- C1 x where
  P x = f (C1 x)

f (P x) = C2 x

In this case, 'P' needs to be typechecked in two passes:

1. Typecheck the pattern definition of 'P', which fully determines the
   type of 'P'. This step doesn't require knowing anything about 'f',
   since the builder definition is not looked at.

2. Typecheck the builder definition, which needs the typechecked
   definition of 'f' to be in scope; done by calls oo tcPatSynBuilderBind
   in TcBinds.tcValBinds.

This behaviour is implemented in 'tcValBinds', but it crucially
depends on 'P' not being put in a recursive group with 'f' (which
would make it look like a recursive pattern synonym a la 'pattern P =
P' which is unsound and rejected).

So I don't see an easy way to give you want you want.

The only think I can think of is to allow some kind of monomorphic recursion. But it's easy to program around, so I'm disinclined to fiddle.

comment:4 Changed 5 months ago by simonpj

adding a type signature won't make the error go away

I didn't claim that it would!

But you give me an idea. If you wrote a pattern signature:

pattern One :: Num a  => a
pattern One <- ((==One) -> True)
  where One = 1

then I think we could soundly suppress the check, without messing up the architecture above. Hmm.

Note: See TracTickets for help on using tickets.