Skip to content

shouldNotTypecheck not catching some deferred type errors #12

@rampion

Description

@rampion

I've found some cases where shouldNotTypecheck fails to capture the deferred type errors. The full error is documented here, but in short, what seems to be happening is:

  • I've got an expression fromNatSingToZ (SuccSing ZeroSing) :: Z 'Zero that fails to typecheck due to a missing instance - shouldNotTypecheck does capture the deferred type error.

  • when I pass that expression to a function fromZToF (fromNatSingToZ (SuccSing ZeroSing)) where fromZToF :: Z 'Zero -> F, shouldNotTypecheck does not capture the deferred type error. It suggests I make sure the expression has a NFData instance, which F does.

There's some other weird behaviour going on:

  • if I rename fromNatSingToZ to toZ, shouldNotTypecheck does capture the deferred type error above, but doesn't capture the deferred type error thrown by fromNatSingToF (SuccSing ZeroSing)) where fromNatSingToF = fromZToF . fromNatSingToZ
  • if I rename the type F to X or G, all the above deferred type errors are captured
  • if I move the module that defines the test from Data/BugSpec.hs to BugSpec.hs, all the above deferred type errors are captured.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions