Opened 10 years ago

Closed 9 years ago

#3651 closed bug (fixed)

GADT type checking too liberal

Reported by: MartijnVanSteenbergen Owned by: simonpj
Priority: normal Milestone: 7.0.1
Component: Compiler (Type checker) Version: 6.10.4
Keywords: Cc: michal.terepeta@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: T3651
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

I would expect the following three functions to fail:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

module Unsafe where

data Z a where
  U :: Z ()
  B :: Z Bool

unsafe1 :: Z a -> Z a -> a
unsafe1 B U = ()

unsafe2 :: a ~ b => Z b -> Z a -> a
unsafe2 B U = ()

unsafe3 :: a ~ b => Z a -> Z b -> a
unsafe3 B U = True

But they are all accepted. In unsafe1 it seems pattern matching on the second argument discards any information learned from pattern matching on the first, while in the other two functions it seems the equality constraints are not checked at all.

Change History (7)

comment:1 Changed 10 years ago by igloo

Milestone: 6.14.1
Type of failure: None/Unknown

These are all accepted in 6.12 and HEAD too, but trying to call any of them with arguments B and U fails:

Couldn't match expected type `Bool' against inferred type `()'

I'm not sure if that's the expected behaviour or not.

comment:2 Changed 9 years ago by michalt

Cc: michal.terepeta@… added

Seems like the new type checker fixes the bug:

  • for unsafe1:
Inaccessible code in
  a pattern with constructor `U', in an equation for `unsafe1'
Couldn't match type `()' with `Bool'
In the pattern: U
In an equation for `unsafe1': unsafe1 B U = ()
  • for unsafe2:
Inaccessible code in
  a pattern with constructor `U', in an equation for `unsafe2'
Couldn't match type `()' with `Bool'
In the pattern: U
In an equation for `unsafe2': unsafe2 B U = ()
  • for unsafe3:
Inaccessible code in
  a pattern with constructor `U', in an equation for `unsafe3'
Couldn't match type `()' with `Bool'
In the pattern: U
In an equation for `unsafe3': unsafe3 B U = True
ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.1.20101008

Not sure whether we should create a new test for this ticket, so I'm leaving it open.

comment:3 Changed 9 years ago by igloo

Owner: set to igloo

Thanks, I'll add a test.

comment:4 Changed 9 years ago by simonpj

I've noticed that only one of the three errors is reported, at a time. I'll fix that.

comment:5 in reply to:  4 Changed 9 years ago by michalt

Replying to simonpj:

I've noticed that only one of the three errors is reported, at a time. I'll fix that.

You're right! I have absolutely no idea why I've tested them one at a time. Sorry if that caused any confusion.

comment:6 Changed 9 years ago by igloo

Owner: changed from igloo to simonpj
Test Case: T3651

Test added, but currently fails due to the "only one of the three errors is reported at a time" problem.

comment:7 Changed 9 years ago by simonpj

Resolution: fixed
Status: newclosed

Fixed. We now get all three errors.

Simon

Note: See TracTickets for help on using tickets.