Opened 5 years ago

Closed 3 years ago

#3169 closed bug (fixed)

Bad occurs-check error message

Reported by: simonpj Owned by:
Priority: low Milestone: 7.0.2
Component: Compiler (Type checker) Version: 6.10.2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: gadt/T3169 Blocked By:
Blocking: Related Tickets:

Description

Consider this:

{-# LANGUAGE  TypeFamilies, ScopedTypeVariables #-}
module Map where

import Prelude hiding ( lookup )

class Key k where
  type Map k :: * -> *
  lookup :: k -> Map k elt -> Maybe elt

instance (Key a, Key b) => Key (a,b) where
  type Map (a,b) = MP a b
  lookup (a,b) (m :: Map (a,b) elt) 
     = case lookup a m :: Maybe (Map b elt) of
	  Just (m2 :: Map b elt) -> lookup b m2 :: Maybe elt

data MP a b elt = MP (Map a (Map b elt))

This ought to typecheck, even in the absence of all those type signatures. But alas:

Map.hs:13:12:
    Occurs check: cannot construct the infinite type: elt = t elt
    In the expression: lookup a m :: Maybe (Map b elt)
    In the expression:
        case lookup a m :: Maybe (Map b elt) of {
          Just (m2 :: Map b elt) -> lookup b m2 :: Maybe elt }

Simon

Change History (8)

comment:1 Changed 5 years ago by chak

  • Resolution set to worksforme
  • Status changed from new to closed

I disagree. GHC is perfectly right. You forgot to match the data constructor MP in the second argument of lookup.

instance (Key a, Key b) => Key (a,b) where
  type Map (a,b) = MP a b
  lookup (a,b) (MP m)
     = case lookup a m of
	  Just m2 -> lookup b m2

works fine for me in the HEAD.

comment:2 Changed 5 years ago by simonpj

  • Component changed from Compiler to Compiler (Type checker)
  • Resolution worksforme deleted
  • Status changed from closed to reopened
  • Summary changed from Type families occurs check to Bad occurs-check error message

Darn! Silly me.

The error message is horrible though:

  • In the call (lookup a m) there's a second error: looking up in m requires a key of type (a,b) but a::a. So a more comprehensible error might be "can't unify a with (a,b)". (Not an occurs-check, but because 'a' is a skolem.) I think with our new "deferring" mechanism we'll be able to defer occurs-check errors and report other errors first.
  • The occurs-check itself is unhelpful. It should really say
        Occurs check: cannot construct the infinite type: elt = Map b elt
        Expected type: Maybe (Map b elt)
        Inferred type: Maybe elt
        In the expression: lookup a m :: Maybe (Map b elt)
    
    Ie not elt = t elt but elt = Map b elt. And showing the expected/inferred types would be helpful.

I'll re-open with a new title!

Simon

comment:3 Changed 5 years ago by simonpj

  • Owner chak deleted
  • Status changed from reopened to new

comment:4 Changed 4 years ago by igloo

  • Milestone changed from 6.12.1 to 6.12 branch
  • Type of failure set to None/Unknown

comment:5 Changed 4 years ago by igloo

  • Milestone changed from 6.12 branch to 6.12.3

comment:6 Changed 4 years ago by igloo

  • Milestone changed from 6.12.3 to 6.14.1
  • Priority changed from normal to low

comment:7 Changed 3 years ago by igloo

  • Milestone changed from 7.0.1 to 7.0.2

comment:8 Changed 3 years ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to gadt/T3169

Happily with the new type checker the error message is almost exactly as I said it should be 22 months ago:

T3169.hs:13:13:
    Couldn't match type `elt' with `Map b elt'
      `elt' is a rigid type variable bound by
            the type signature for
              lookup :: (a, b) -> Map (a, b) elt -> Maybe elt
            at T3169.hs:12:3
    Expected type: Maybe (Map b elt)
      Actual type: Maybe elt
    In the return type of a call of `lookup'
    In the expression: lookup a m :: Maybe (Map b elt)

I've added a regression test, and will close.

Note: See TracTickets for help on using tickets.