Opened 12 months ago

Last modified 6 months ago

#9260 new bug

Unnecessary error using GHC.TypeLits

Reported by: Iceland_jack Owned by: diatchki
Priority: low Milestone: 7.12.1
Component: Compiler Version: 7.8.2
Keywords: type lits, data kinds, error message Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description (last modified by thomie)

Compiling:

{-# LANGUAGE DataKinds, TypeOperators, GADTs #-}

module Error where

import GHC.TypeLits

data Fin n where
  Fzero :: Fin (n + 1)
  Fsucc :: Fin n -> Fin (n + 1)

test :: Fin 1
test = Fsucc Fzero

gives a strange (unnecessary) error message claiming that Fin 1 doesn't match the expected type Fin (0 + 1):

% ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.8.2
% ghc -ignore-dot-ghci /tmp/Error.hs
[1 of 1] Compiling Error            ( /tmp/Error.hs, /tmp/Error.o )

/tmp/Error.hs:12:8:
    Couldn't match type ‘0’ with ‘1’
    Expected type: Fin 1
      Actual type: Fin (0 + 1)
    In the expression: Fsucc Fzero
    In an equation for ‘test’: test = Fsucc Fzero

/tmp/Error.hs:12:14:
    Couldn't match type ‘1’ with ‘0’
    Expected type: Fin 0
      Actual type: Fin (0 + 1)
    In the first argument of ‘Fsucc’, namely ‘Fzero’
    In the expression: Fsucc Fzero
%

Change History (6)

comment:1 Changed 12 months ago by Iceland_jack

Forgot to add the actual failing case:

test :: Fin 1
test = Fsucc Fzero

comment:2 Changed 12 months ago by goldfire

The first error you report is certainly a bug. But, the second one is legitimate -- the type Fin 1 has only 1 inhabitant, Fzero.

Confirmed reproducible in HEAD.

comment:3 Changed 12 months ago by Iceland_jack

Yes the second error is expected, the bug seems to occur for any finite set that is too small except the smallest example:

Fzero :: Fin 0

comment:4 Changed 10 months ago by simonpj

  • Owner set to diatchki

Iavor, might you look at this, as Mr type-lits? Thanks!

Simon

comment:5 Changed 8 months ago by thomie

  • Description modified (diff)
  • Milestone set to 7.10.1
  • Operating System changed from Linux to Unknown/Multiple

GHC HEAD now gives the following error message for the program from the description:

$ ghc-7.9.20141113 test.hs
[1 of 1] Compiling Test             ( test.hs, test.o )

test.hs:12:14:
    Couldn't match type ‘n0 + 1’ with ‘0’
    The type variable ‘n0’ is ambiguous
    Expected type: Fin 0
      Actual type: Fin (n0 + 1)
    In the first argument of ‘Fsucc’, namely ‘Fzero’
    In the expression: Fsucc Fzero

It looks like this bug got fixed, but I'm not 100% sure. A regression test is still missing.

comment:6 Changed 6 months ago by thoughtpolice

  • Milestone changed from 7.10.1 to 7.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

Note: See TracTickets for help on using tickets.